tuned;

--- a/src/HOL/ex/ML.thy	Mon Nov 30 13:16:12 2015 +0100
+++ b/src/HOL/ex/ML.thy	Mon Nov 30 14:24:51 2015 +0100
@@ -11,8 +11,8 @@
 section \<open>ML expressions\<close>
 
 text \<open>
-  The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal
-  text. It is type-checked, compiled, and run within that environment.
+  The Isabelle command \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the
+  formal text. It is type-checked, compiled, and run within that environment.
 
   Note that side-effects should be avoided, unless the intention is to change
   global parameters of the run-time environment (rare).
@@ -29,8 +29,10 @@
 
 section \<open>Antiquotations\<close>
 
-text \<open>There are some language extensions (via antiquotations), as explained in
-  the ``Isabelle/Isar implementation manual'', chapter 0.\<close>
+text \<open>
+  There are some language extensions (via antiquotations), as explained in the
+  ``Isabelle/Isar implementation manual'', chapter 0.
+\<close>
 
 ML \<open>length []\<close>
 ML \<open>@{assert} (length [] = 0)\<close>
@@ -39,23 +41,33 @@
 text \<open>Formal entities from the surrounding context may be referenced as
   follows:\<close>
 
-term "1 + 1"   -- \<open>term within theory source\<close>
+term "1 + 1"   \<comment> \<open>term within theory source\<close>
 
 ML \<open>@{term "1 + 1"}   (* term as symbolic ML datatype value *)\<close>
 
 ML \<open>@{term "1 + (1::int)"}\<close>
 
 
+ML \<open>
+  (* formal source with position information *)
+  val s = \<open>1 + 1\<close>;
+
+  (* read term via old-style string interface *)
+  val t = Syntax.read_term @{context} (Syntax.implode_input s);
+\<close>
+
 section \<open>IDE support\<close>
 
 text \<open>
   ML embedded into the Isabelle environment is connected to the Prover IDE.
   Poly/ML provides:
-  \begin{itemize}
-    \item precise positions for warnings / errors
-    \item markup for defining positions of identifiers
-    \item markup for inferred types of sub-expressions
-  \end{itemize}
+
+    \<^item> precise positions for warnings / errors
+    \<^item> markup for defining positions of identifiers
+    \<^item> markup for inferred types of sub-expressions
+    \<^item> pretty-printing of ML values with markup
+    \<^item> completion of ML names
+    \<^item> source-level debugger
 \<close>
 
 ML \<open>fn i => fn list => length list + i\<close>
@@ -87,9 +99,10 @@
 text \<open>
   Future.fork/join/cancel manage parallel evaluation.
 
-  Note that within Isabelle theory documents, the top-level command boundary may
-  not be transgressed without special precautions. This is normally managed by
-  the system when performing parallel proof checking.\<close>
+  Note that within Isabelle theory documents, the top-level command boundary
+  may not be transgressed without special precautions. This is normally
+  managed by the system when performing parallel proof checking.
+\<close>
 
 ML \<open>
   val x = Future.fork (fn () => ackermann 3 10);
@@ -97,8 +110,10 @@
   val z = Future.join x + Future.join y
 \<close>
 
-text \<open>The @{ML_structure Par_List} module provides high-level combinators
-  for parallel list operations.\<close>
+text \<open>
+  The @{ML_structure Par_List} module provides high-level combinators for
+  parallel list operations.
+\<close>
 
 ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
 ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
@@ -111,12 +126,12 @@
   "factorial 0 = 1"
 | "factorial (Suc n) = Suc n * factorial n"
 
-term "factorial 4"  -- \<open>symbolic term\<close>
-value "factorial 4"  -- \<open>evaluation via ML code generation in the background\<close>
+term "factorial 4"  \<comment> \<open>symbolic term\<close>
+value "factorial 4"  \<comment> \<open>evaluation via ML code generation in the background\<close>
 
 declare [[ML_source_trace]]
-ML \<open>@{term "factorial 4"}\<close>  -- \<open>symbolic term in ML\<close>
-ML \<open>@{code "factorial"}\<close>  -- \<open>ML code from function specification\<close>
+ML \<open>@{term "factorial 4"}\<close>  \<comment> \<open>symbolic term in ML\<close>
+ML \<open>@{code "factorial"}\<close>  \<comment> \<open>ML code from function specification\<close>
 
 
 fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"

--- a/src/Tools/SML/Examples.thy	Mon Nov 30 13:16:12 2015 +0100
+++ b/src/Tools/SML/Examples.thy	Mon Nov 30 14:24:51 2015 +0100
@@ -9,12 +9,12 @@
 begin
 
 text \<open>
-  Isabelle/ML is a somewhat augmented version of Standard ML, with
-  various add-ons that are indispensable for Isabelle development, but
-  may cause conflicts with independent projects in plain Standard ML.
+  Isabelle/ML is a somewhat augmented version of Standard ML, with various
+  add-ons that are indispensable for Isabelle development, but may cause
+  conflicts with independent projects in plain Standard ML.
 
-  The Isabelle/Isar command 'SML_file' supports official Standard ML
-  within the Isabelle environment, with full support in the Prover IDE
+  The Isabelle/Isar command \<^theory_text>\<open>SML_file\<close> supports official Standard ML within
+  the Isabelle environment, with full support in the Prover IDE
   (Isabelle/jEdit).
 
   Here is a very basic example that defines the factorial function and
@@ -24,10 +24,10 @@
 SML_file "factorial.sml"
 
 text \<open>
-  The subsequent example illustrates the use of multiple 'SML_file'
-  commands to build larger Standard ML projects.  The toplevel SML
-  environment is enriched cumulatively within the theory context of
-  Isabelle --- independently of the Isabelle/ML environment.
+  The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands
+  to build larger Standard ML projects. The toplevel SML environment is
+  enriched cumulatively within the theory context of Isabelle ---
+  independently of the Isabelle/ML environment.
 \<close>
 
 SML_file "Example.sig"
@@ -36,17 +36,17 @@
 
 text \<open>
   Isabelle/ML and SML share a common run-time system, but the static
-  environments are separate.  It is possible to exchange toplevel bindings
-  via separate commands like this.
+  environments are separate. It is possible to exchange toplevel bindings via
+  separate commands like this.
 \<close>
 
-SML_export \<open>val f = factorial\<close>  -- \<open>re-use factorial from SML environment\<close>
+SML_export \<open>val f = factorial\<close>  \<comment> \<open>re-use factorial from SML environment\<close>
 ML \<open>f 42\<close>
 
 SML_import \<open>val println = Output.writeln\<close>
-  -- \<open>re-use Isabelle/ML channel for SML\<close>
+  \<comment> \<open>re-use Isabelle/ML channel for SML\<close>
 
 SML_import \<open>val par_map = Par_List.map\<close>
-  -- \<open>re-use Isabelle/ML parallel list combinator for SML\<close>
+  \<comment> \<open>re-use Isabelle/ML parallel list combinator for SML\<close>
 
 end