added ML antiquotation @{print};

--- a/NEWS	Fri Apr 04 10:41:53 2014 +0200
+++ b/NEWS	Fri Apr 04 12:07:48 2014 +0200
@@ -642,6 +642,10 @@
 well-defined master directory, so an absolute symbolic path
 specification is usually required, e.g. "~~/src/HOL".
 
+* ML antiquotation @{print} inlines a function to print an arbitrary
+ML value, which is occasionally useful for diagnostic or demonstration
+purposes.
+
 
 *** System ***
 

--- 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};
 *}
 
 

--- a/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 10:41:53 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 12:07:48 2014 +0200
@@ -8,12 +8,7 @@
 struct
 
 val _ = Theory.setup
- (ML_Antiquotation.inline @{binding assert}
-    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
-
-  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
-
-  ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
+ (ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
     (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
      ML_Syntax.print_string name))) #>
 
@@ -56,6 +51,30 @@
           ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
+(* ML support *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding assert}
+    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
+
+  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
+
+  ML_Antiquotation.declaration @{binding print}
+    (Scan.lift (Scan.optional Args.name "Output.writeln"))
+      (fn src => fn output => fn ctxt =>
+        let
+          val (_, pos) = Args.name_of_src src;
+          val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
+          val env =
+            "val " ^ a ^ ": string -> unit =\n\
+            \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
+            ML_Syntax.print_position pos ^ "));\n";
+          val body =
+            "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
+        in (K (env, body), ctxt') end));
+
+  
+
 (* type classes *)
 
 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>