# HG changeset patch
# User wenzelm
# Date 1535403516 -7200
# Node ID 7414ce0256e1112e0124b425c4a5e39f38c49d9f
# Parent  5e7b1ae10eb8d554204f5825418fb3d9319d6281
some NEWS (instead of proper documentation);

diff -r 5e7b1ae10eb8 -r 7414ce0256e1 NEWS
--- a/NEWS	Mon Aug 27 20:43:01 2018 +0200
+++ b/NEWS	Mon Aug 27 22:58:36 2018 +0200
@@ -28,6 +28,25 @@
 * Original PolyML.pointerEq is retained as a convenience for tools that
 don't use Isabelle/ML (where this is called "pointer_eq").
 
+* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
+option ML_environment to select a named environment, such as "Isabelle"
+for Isabelle/ML, or "SML" for official Standard ML. It is also possible
+to move toplevel bindings between environments, using a notation with
+">" as separator. For example:
+
+  declare [[ML_environment = "Isabelle>SML"]]
+  ML \<open>val println = writeln\<close>
+
+  declare [[ML_environment = "SML"]]
+  ML \<open>println "test"\<close>
+
+  declare [[ML_environment = "Isabelle"]]
+  ML \<open>println\<close>  \<comment> \<open>not present\<close>
+
+The Isabelle/ML function ML_Env.setup defines new ML environments. This
+is useful to incorporate big SML projects in an isolated name space, and
+potentially with variations on ML syntax (existing ML_Env.SML_operations
+observes the official standard).
 
 
 New in Isabelle2018 (August 2018)