[isabelle-dev] NEWS: Isabelle support for Standard ML

[Makarius]

On Tue, 25 Mar 2014, Makarius wrote:

> * Command 'SML_file' reads and evaluates the given Standard ML file.
> Toplevel bindings are stored within the theory context; the initial
> environment is restricted to the Standard ML implementation of
> Poly/ML, without the add-ons of Isabelle/ML.  See also
> ~/src/Tools/SML/Examples.thy for some basic examples.

Just a minor update in Isabelle/874bdedb2313:

* Support for official Standard ML within the Isabelle context.
Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
and 'SML_export' allow to exchange toplevel bindings between the two
separate environments.  See also ~~/src/Tools/SML/Examples.thy for
some examples.


The updated examples cover SML_import and SML_export as well.  The latter 
might be useful in loading big chunks of official Standard ML, without 
going through the pain to make it conform to Isabelle/ML. A few result 
structures or functions for Isabelle/ML can be harvested from the SML 
environment in the end.

Nonetheless, such SML applications (especially SML/NJ ones) need to 
conform semantically to the Isabelle runtime environment: global refs or 
Gansner-Reppy style catch-all exception handlers won't work without the 
special assumption of sequentialism and non-interruption.


 	Makarius