# HG changeset patch
# User wenzelm
# Date 1365428148 -7200
# Node ID e49bf0be79ba61869f2858ae4830f23527b42b34
# Parent  e8e027aa694f8845ea4e8ca5f59a79bb2781e697
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);

diff -r e8e027aa694f -r e49bf0be79ba src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Mon Apr 08 14:28:37 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Mon Apr 08 15:35:48 2013 +0200
@@ -740,6 +740,46 @@
 *}
 
 
+subsection {* Printing ML values *}
+
+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.  *}
+
+text %mlantiq {*
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
+  \end{matharray}
+
+  @{rail "
+  @@{ML_antiquotation make_string}
+  "}
+
+  \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.
+
+  \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.  *}
+
+ML {*
+  val x = 42;
+  val y = true;
+
+  writeln (@{make_string} {x = x, y = y});
+*}
+
+
 section {* Canonical argument order \label{sec:canonical-argument-order} *}
 
 text {* Standard ML is a language in the tradition of @{text