# HG changeset patch
# User wenzelm
# Date 1395939373 -3600
# Node ID 40274e4f5ebf9e3d77d07b985e7a7d8e972176e6
# Parent  4cc3f4db3447fc9f50ce194e00e7a12bbc08b64e
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
more explicit ML_Compiler.flags;

diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -100,8 +100,7 @@
       val txt' = if kind = "" then txt else kind ^ " " ^ txt;
 
       val _ =
-        ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1)
-          (ml (toks1, toks2));
+        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2));
       val kind' = if kind = "" then "ML" else "ML " ^ kind;
     in
       "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Mar 27 17:56:13 2014 +0100
@@ -120,7 +120,7 @@
           ML_Lex.read Position.none "fn _ => (" @
           ML_Lex.read_source false source @
           ML_Lex.read Position.none ");";
-        val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
+        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks;
       in "" end);
 *}
 
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/General/output.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -30,8 +30,6 @@
   val error_message: string -> unit
   val prompt: string -> unit
   val status: string -> unit
-  val direct_report: string -> unit
-  val redirect_report: (string -> unit) -> ('a -> 'b) -> 'a -> 'b
   val report: string -> unit
   val result: Properties.T -> string -> unit
   val protocol_message: Properties.T -> string -> unit
@@ -117,17 +115,7 @@
 fun error_message s = error_message' (serial (), s);
 fun prompt s = ! prompt_fn (output s);
 fun status s = ! status_fn (output s);
-
-fun direct_report s = ! report_fn (output s);
-
-local
-  val tag = Universal.tag () : (string -> unit) Universal.tag;
-  fun thread_data () = the_default direct_report (Thread.getLocal tag);
-in
-  fun redirect_report rep = Library.setmp_thread_data tag (thread_data ()) rep;
-  fun report s = thread_data () s;
-end;
-
+fun report s = ! report_fn (output s);
 fun result props s = ! result_fn props (output s);
 fun protocol_message props s = ! protocol_message_fn props (output s);
 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -145,8 +145,10 @@
         \  val " ^ name ^
         " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
         \end;\n");
-    val flags = {SML = false, verbose = false};
-  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
+  in
+    Context.theory_map
+      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants))
+  end;
 
 
 (* old-style defs *)
@@ -236,10 +238,12 @@
 );
 
 fun ml_diag verbose source = Toplevel.keep (fn state =>
-  let val opt_ctxt =
-    try Toplevel.generic_theory_of state
-    |> Option.map (Context.proof_of #> Diag_State.put state)
-  in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
+  let
+    val opt_ctxt =
+      try Toplevel.generic_theory_of state
+      |> Option.map (Context.proof_of #> Diag_State.put state);
+    val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
+  in ML_Context.eval_source_in opt_ctxt flags source end);
 
 val diag_state = Diag_State.get;
 
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -273,23 +273,26 @@
         let
           val ([{lines, pos, ...}], thy') = files thy;
           val source = {delimited = true, text = cat_lines lines, pos = pos};
+          val flags = {SML = true, redirect = true, verbose = true};
         in
           thy' |> Context.theory_map
-            (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
+            (ML_Context.exec (fn () => ML_Context.eval_source flags source))
         end)));
 
 val _ =
   Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
+        (ML_Context.exec (fn () =>
+            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
           Local_Theory.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
     (Parse.ML_source >> (fn source =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
+        (ML_Context.exec (fn () =>
+            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #>
           Proof.propagate_ml_env)));
 
 val _ =
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -6,22 +6,26 @@
 
 signature ML_COMPILER =
 sig
-  type flags = {SML: bool, verbose: bool}
+  type flags = {SML: bool, redirect: bool, verbose: bool}
+  val flags: flags
+  val verbose: bool -> flags -> flags
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
 end
 
 structure ML_Compiler: ML_COMPILER =
 struct
 
-type flags = {SML: bool, verbose: bool};
+type flags = {SML: bool, redirect: bool, verbose: bool};
+val flags = {SML = false, redirect = false, verbose = false};
+fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
 
-fun eval {SML, verbose} pos toks =
+fun eval (flags: flags) pos toks =
   let
-    val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
+    val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
     val line = the_default 1 (Position.line_of pos);
     val file = the_default "ML" (Position.file_of pos);
     val text = ML_Lex.flatten toks;
-  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
+  in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end;
 
 end;
 
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -12,42 +12,65 @@
 
 (* parse trees *)
 
-fun report_parse_tree depth space =
+fun report_parse_tree redirect depth space parse_tree =
   let
-    val reported_text =
+    val is_visible =
       (case Context.thread_data () of
-        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
-      | _ => Position.reported_text);
+        SOME context => Context_Position.is_visible_generic context
+      | NONE => true);
+    fun is_reported pos = is_visible andalso Position.is_reported pos;
+
+    fun reported_types loc types =
+      let val pos = Exn_Properties.position_of loc in
+        is_reported pos ?
+          let
+            val xml =
+              PolyML.NameSpace.displayTypeExpression (types, depth, space)
+              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+              |> Output.output |> YXML.parse_body;
+          in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
+      end;
 
     fun reported_entity kind loc decl =
-      reported_text (Exn_Properties.position_of loc)
-        (Markup.entityN,
-          (Markup.kindN, kind) :: Position.def_properties_of (Exn_Properties.position_of decl)) "";
+      let val pos = Exn_Properties.position_of loc in
+        is_reported pos ?
+          let
+            val def_pos = Exn_Properties.position_of decl;
+            fun markup () =
+              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
+          in cons (pos, markup, fn () => "") end
+      end;
 
-    fun reported loc (PolyML.PTtype types) =
-          cons
-            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
-              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-              |> reported_text (Exn_Properties.position_of loc) Markup.ML_typing)
-      | reported loc (PolyML.PTdeclaredAt decl) =
-          cons (reported_entity Markup.ML_defN loc decl)
-      | reported loc (PolyML.PTopenedAt decl) =
-          cons (reported_entity Markup.ML_openN loc decl)
-      | reported loc (PolyML.PTstructureAt decl) =
-          cons (reported_entity Markup.ML_structureN loc decl)
+    fun reported loc (PolyML.PTtype types) = reported_types loc types
+      | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
+      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
+      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
       | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
       | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
       | reported _ _ = I
     and reported_tree (loc, props) = fold (reported loc) props;
-  in fn tree => Output.report (implode (reported_tree tree [])) end;
+
+    val persistent_reports = reported_tree parse_tree [];
+
+    fun output () =
+      persistent_reports
+      |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
+      |> implode |> Output.report;
+  in
+    if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+    then
+      Execution.print {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1}
+        (fn _ => output ())
+    else output ()
+  end;
 
 
 (* eval ML source tokens *)
 
-fun eval {SML, verbose} pos toks =
+fun eval (flags: flags) pos toks =
   let
     val _ = Secure.secure_mltext ();
-    val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
+    val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space;
     val opt_context = Context.thread_data ();
 
 
@@ -133,7 +156,7 @@
     fun result_fun (phase1, phase2) () =
      ((case phase1 of
         NONE => ()
-      | SOME parse_tree => report_parse_tree depth space parse_tree);
+      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
       (case phase2 of
         NONE => raise STATIC_ERRORS ()
       | SOME code =>
@@ -171,7 +194,7 @@
             val _ = output_writeln ();
           in raise_error exn_msg end;
   in
-    if verbose then (output_warnings (); flush_error (); output_writeln ())
+    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
     else ()
   end;
 
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -137,7 +137,7 @@
 
 fun eval flags pos ants =
   let
-    val non_verbose = {SML = #SML flags, verbose = false};
+    val non_verbose = ML_Compiler.verbose false flags;
 
     (*prepare source text*)
     val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
@@ -181,13 +181,14 @@
     (fn () => eval_source flags source) ();
 
 fun expression pos bind body ants =
-  exec (fn () => eval {SML = false, verbose = false} pos
-    (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
+  exec (fn () =>
+    eval ML_Compiler.flags pos
+     (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
       ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
 
 end;
 
 fun use s =
-  ML_Context.eval_file {SML = false, verbose = true} (Path.explode s)
+  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
     handle ERROR msg => (writeln msg; error "ML error");
 
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -130,7 +130,7 @@
       else if not (ML_Syntax.is_identifier name) then
         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
       else
-        ML_Compiler.eval {SML = false, verbose = true} Position.none
+        ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
           (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
     val _ = Theory.setup (Stored_Thms.put []);
   in () end;
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/PIDE/execution.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -18,7 +18,6 @@
   type params = {name: string, pos: Position.T, pri: int}
   val fork: params -> (unit -> 'a) -> 'a future
   val print: params -> (serial -> unit) -> unit
-  val print_report: string -> unit
   val fork_prints: Document_ID.exec -> unit
   val purge: Document_ID.exec list -> unit
   val reset: unit -> Future.group list
@@ -148,14 +147,6 @@
       | NONE => raise Fail (unregistered exec_id))
     end));
 
-fun print_report s =
-  if s = "" orelse not (Multithreading.enabled ()) then Output.direct_report s
-  else
-    let
-      val body = YXML.parse_body s  (*sharable closure!*)
-      val params = {name = "", pos = Position.thread_data (), pri = 0};
-    in print params (fn _ => Output.direct_report (YXML.string_of_body body)) end;
-
 fun fork_prints exec_id =
   (case Inttab.lookup (#2 (get_state ())) exec_id of
     SOME (_, prints) =>
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -639,7 +639,7 @@
 
 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
   (fn {context, ...} => fn source =>
-   (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
+   (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
     Symbol_Pos.source_content source
     |> #1
     |> (if Config.get context quotes then quote else I)
diff -r 4cc3f4db3447 -r 40274e4f5ebf src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/pure_syn.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -23,9 +23,10 @@
           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
           val provide = Resources.provide (src_path, digest);
           val source = {delimited = true, text = cat_lines lines, pos = pos};
+          val flags = {SML = false, redirect = true, verbose = true};
         in
           gthy
-          |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source)
+          |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
           |> Local_Theory.propagate_ml_env
           |> Context.mapping provide (Local_Theory.background_theory provide)
         end)));