# HG changeset patch
# User wenzelm
# Date 1557477698 -7200
# Node ID 22cfcfcadd8b058215b706caf714cd55d0dc60d0
# Parent  42f73412fa06c6b6cd514e922844b9e079b4517e
more documentation;

diff -r 42f73412fa06 -r 22cfcfcadd8b NEWS
--- a/NEWS	Thu May 09 16:48:25 2019 +0200
+++ b/NEWS	Fri May 10 10:41:38 2019 +0200
@@ -317,25 +317,9 @@
 See also commands 'export_generated_files' and 'compile_generated_files'
 to use the results.
 
-* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
+* ML evaluation (notably via command 'ML' or '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).
+for Isabelle/ML, or "SML" for official Standard ML.
 
 * ML antiquotation @{master_dir} refers to the master directory of the
 underlying theory, i.e. the directory of the theory file.
diff -r 42f73412fa06 -r 22cfcfcadd8b src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu May 09 16:48:25 2019 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri May 10 10:41:38 2019 +0200
@@ -1071,6 +1071,7 @@
     @{attribute_def ML_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def ML_exception_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def ML_exception_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
+    @{attribute_def ML_environment} & : & \<open>attribute\<close> & default \<open>Isabelle\<close> \\
   \end{tabular}
 
   \<^rail>\<open>
@@ -1185,8 +1186,37 @@
   the Poly/ML debugger, at the cost of extra compile-time and run-time
   overhead. Relevant ML modules need to be compiled beforehand with debugging
   enabled, see @{attribute ML_debugger} above.
+
+  \<^descr> @{attribute ML_environment} determines the named ML environment for
+  toplevel declarations, e.g.\ in command \<^theory_text>\<open>ML\<close> or \<^theory_text>\<open>ML_file\<close>. The following
+  ML environments are predefined in Isabelle/Pure:
+
+    \<^item> \<open>Isabelle\<close> for Isabelle/ML. It contains all modules of Isabelle/Pure and
+    further add-ons, e.g. material from Isabelle/HOL.
+
+    \<^item> \<open>SML\<close> for official Standard ML. It contains only the initial basis
+    according to \<^url>\<open>http://sml-family.org/Basis/overview.html\<close>.
+
+  The Isabelle/ML function \<^ML>\<open>ML_Env.setup\<close> defines a new ML environment.
+  This is useful to incorporate big SML projects in an isolated name space,
+  possibly with variations on ML syntax; the existing setup of
+  \<^ML>\<open>ML_Env.SML_operations\<close> follows the official standard.
+
+  It is also possible to move toplevel bindings between ML environments, using
+  a notation with ``\<open>>\<close>'' as separator. For example:
 \<close>
 
+(*<*)experiment begin(*>*)
+        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>ML \<open>println\<close> (*bad*) handle ERROR msg => warning msg\<close>
+(*<*)end(*>*)
+
 
 section \<open>Generated files and external files\<close>