NEWS
changeset 68824 7414ce0256e1
parent 68803 169bf32b35dd
child 68848 8825efd1c2cf
     1.1 --- a/NEWS	Mon Aug 27 20:43:01 2018 +0200
     1.2 +++ b/NEWS	Mon Aug 27 22:58:36 2018 +0200
     1.3 @@ -28,6 +28,25 @@
     1.4  * Original PolyML.pointerEq is retained as a convenience for tools that
     1.5  don't use Isabelle/ML (where this is called "pointer_eq").
     1.6  
     1.7 +* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
     1.8 +option ML_environment to select a named environment, such as "Isabelle"
     1.9 +for Isabelle/ML, or "SML" for official Standard ML. It is also possible
    1.10 +to move toplevel bindings between environments, using a notation with
    1.11 +">" as separator. For example:
    1.12 +
    1.13 +  declare [[ML_environment = "Isabelle>SML"]]
    1.14 +  ML \<open>val println = writeln\<close>
    1.15 +
    1.16 +  declare [[ML_environment = "SML"]]
    1.17 +  ML \<open>println "test"\<close>
    1.18 +
    1.19 +  declare [[ML_environment = "Isabelle"]]
    1.20 +  ML \<open>println\<close>  \<comment> \<open>not present\<close>
    1.21 +
    1.22 +The Isabelle/ML function ML_Env.setup defines new ML environments. This
    1.23 +is useful to incorporate big SML projects in an isolated name space, and
    1.24 +potentially with variations on ML syntax (existing ML_Env.SML_operations
    1.25 +observes the official standard).
    1.26  
    1.27  
    1.28  New in Isabelle2018 (August 2018)