src/Doc/IsarImplementation/ML.thy

--- a/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 10:41:53 2014 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 12:07:48 2014 +0200
@@ -690,38 +690,52 @@
 text {* The ML compiler knows about the structure of values according
   to their static type, and can print them in the manner of the
   toplevel loop, although the details are non-portable.  The
-  antiquotation @{ML_antiquotation_def "make_string"} provides a
-  quasi-portable way to refer to this potential capability of the
-  underlying ML system in generic Isabelle/ML sources.  *}
+  antiquotations @{ML_antiquotation_def "make_string"} and
+  @{ML_antiquotation_def "print"} provide a quasi-portable way to
+  refer to this potential capability of the underlying ML system in
+  generic Isabelle/ML sources.
+
+  This is occasionally useful for diagnostic or demonstration
+  purposes.  Note that production-quality tools require proper
+  user-level error messages. *}
 
 text %mlantiq {*
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
+  @{ML_antiquotation_def "print"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
   @{rail \<open>
   @@{ML_antiquotation make_string}
+  ;
+  @@{ML_antiquotation print} @{syntax name}?
   \<close>}
 
   \begin{description}
 
   \item @{text "@{make_string}"} inlines a function to print arbitrary
-values similar to the ML toplevel.  The result is compiler dependent
-and may fall back on "?" in certain situations.
+  values similar to the ML toplevel.  The result is compiler dependent
+  and may fall back on "?" in certain situations.
+
+  \item @{text "@{print f}"} uses the ML function @{text "f: string ->
+  unit"} to output the result of @{text "@{make_string}"} above,
+  together with the source position of the antiquotation.  The default
+  output function is @{ML writeln}.
 
   \end{description}
 *}
 
-text %mlex {* The following artificial example shows how to produce
-  ad-hoc output of ML values for debugging purposes.  This should not
-  be done in production code, and not persist in regular Isabelle/ML
-  sources.  *}
+text %mlex {* The following artificial examples show how to produce
+  adhoc output of ML values for debugging purposes. *}
 
 ML {*
   val x = 42;
   val y = true;
 
   writeln (@{make_string} {x = x, y = y});
+
+  @{print} {x = x, y = y};
+  @{print tracing} {x = x, y = y};
 *}