# HG changeset patch
# User wenzelm
# Date 1396607877 -7200
# Node ID f0bd809b5d35f827fb8f3c22c8c00970b407b96d
# Parent  6e08b45432f676ff99660752977bcc0037094ae1# Parent  386e4cb7ad68b695399e43c09fea544edb53fda6
merged

diff -r 6e08b45432f6 -r f0bd809b5d35 NEWS
--- a/NEWS	Fri Apr 04 11:49:47 2014 +0200
+++ b/NEWS	Fri Apr 04 12:37:57 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 ***
 
diff -r 6e08b45432f6 -r f0bd809b5d35 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 11:49:47 2014 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 12:37:57 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};
 *}
 
 
diff -r 6e08b45432f6 -r f0bd809b5d35 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 11:49:47 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 12:37:57 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) =>
diff -r 6e08b45432f6 -r f0bd809b5d35 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Apr 04 11:49:47 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Apr 04 12:37:57 2014 +0200
@@ -187,7 +187,7 @@
         }
       }
 
-      private val block_size = 1024
+      private val block_size = 256
     }
 
     final class Commands private(val commands: Linear_Set[Command])