1.1 --- a/src/Doc/antiquote_setup.ML	Thu Mar 27 17:12:40 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Thu Mar 27 17:56:13 2014 +0100
     1.3 @@ -100,8 +100,7 @@
     1.4        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     1.5  
     1.6        val _ =
     1.7 -        ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1)
     1.8 -          (ml (toks1, toks2));
     1.9 +        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2));
    1.10        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.11      in
    1.12        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^

     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Thu Mar 27 17:12:40 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Mar 27 17:56:13 2014 +0100
     2.3 @@ -120,7 +120,7 @@
     2.4            ML_Lex.read Position.none "fn _ => (" @
     2.5            ML_Lex.read_source false source @
     2.6            ML_Lex.read Position.none ");";
     2.7 -        val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
     2.8 +        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks;
     2.9        in "" end);
    2.10  *}
    2.11  

     3.1 --- a/src/Pure/General/output.ML	Thu Mar 27 17:12:40 2014 +0100
     3.2 +++ b/src/Pure/General/output.ML	Thu Mar 27 17:56:13 2014 +0100
     3.3 @@ -30,8 +30,6 @@
     3.4    val error_message: string -> unit
     3.5    val prompt: string -> unit
     3.6    val status: string -> unit
     3.7 -  val direct_report: string -> unit
     3.8 -  val redirect_report: (string -> unit) -> ('a -> 'b) -> 'a -> 'b
     3.9    val report: string -> unit
    3.10    val result: Properties.T -> string -> unit
    3.11    val protocol_message: Properties.T -> string -> unit
    3.12 @@ -117,17 +115,7 @@
    3.13  fun error_message s = error_message' (serial (), s);
    3.14  fun prompt s = ! prompt_fn (output s);
    3.15  fun status s = ! status_fn (output s);
    3.16 -
    3.17 -fun direct_report s = ! report_fn (output s);
    3.18 -
    3.19 -local
    3.20 -  val tag = Universal.tag () : (string -> unit) Universal.tag;
    3.21 -  fun thread_data () = the_default direct_report (Thread.getLocal tag);
    3.22 -in
    3.23 -  fun redirect_report rep = Library.setmp_thread_data tag (thread_data ()) rep;
    3.24 -  fun report s = thread_data () s;
    3.25 -end;
    3.26 -
    3.27 +fun report s = ! report_fn (output s);
    3.28  fun result props s = ! result_fn props (output s);
    3.29  fun protocol_message props s = ! protocol_message_fn props (output s);
    3.30  fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();

     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 17:12:40 2014 +0100
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 17:56:13 2014 +0100
     4.3 @@ -145,8 +145,10 @@
     4.4          \  val " ^ name ^
     4.5          " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
     4.6          \end;\n");
     4.7 -    val flags = {SML = false, verbose = false};
     4.8 -  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
     4.9 +  in
    4.10 +    Context.theory_map
    4.11 +      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants))
    4.12 +  end;
    4.13  
    4.14  
    4.15  (* old-style defs *)
    4.16 @@ -236,10 +238,12 @@
    4.17  );
    4.18  
    4.19  fun ml_diag verbose source = Toplevel.keep (fn state =>
    4.20 -  let val opt_ctxt =
    4.21 -    try Toplevel.generic_theory_of state
    4.22 -    |> Option.map (Context.proof_of #> Diag_State.put state)
    4.23 -  in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
    4.24 +  let
    4.25 +    val opt_ctxt =
    4.26 +      try Toplevel.generic_theory_of state
    4.27 +      |> Option.map (Context.proof_of #> Diag_State.put state);
    4.28 +    val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
    4.29 +  in ML_Context.eval_source_in opt_ctxt flags source end);
    4.30  
    4.31  val diag_state = Diag_State.get;
    4.32  

     5.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 27 17:12:40 2014 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 27 17:56:13 2014 +0100
     5.3 @@ -273,23 +273,26 @@
     5.4          let
     5.5            val ([{lines, pos, ...}], thy') = files thy;
     5.6            val source = {delimited = true, text = cat_lines lines, pos = pos};
     5.7 +          val flags = {SML = true, redirect = true, verbose = true};
     5.8          in
     5.9            thy' |> Context.theory_map
    5.10 -            (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
    5.11 +            (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    5.12          end)));
    5.13  
    5.14  val _ =
    5.15    Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
    5.16      (Parse.ML_source >> (fn source =>
    5.17        Toplevel.generic_theory
    5.18 -        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
    5.19 +        (ML_Context.exec (fn () =>
    5.20 +            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
    5.21            Local_Theory.propagate_ml_env)));
    5.22  
    5.23  val _ =
    5.24    Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
    5.25      (Parse.ML_source >> (fn source =>
    5.26        Toplevel.proof (Proof.map_context (Context.proof_map
    5.27 -        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
    5.28 +        (ML_Context.exec (fn () =>
    5.29 +            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #>
    5.30            Proof.propagate_ml_env)));
    5.31  
    5.32  val _ =

     6.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Mar 27 17:12:40 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 27 17:56:13 2014 +0100
     6.3 @@ -6,22 +6,26 @@
     6.4  
     6.5  signature ML_COMPILER =
     6.6  sig
     6.7 -  type flags = {SML: bool, verbose: bool}
     6.8 +  type flags = {SML: bool, redirect: bool, verbose: bool}
     6.9 +  val flags: flags
    6.10 +  val verbose: bool -> flags -> flags
    6.11    val eval: flags -> Position.T -> ML_Lex.token list -> unit
    6.12  end
    6.13  
    6.14  structure ML_Compiler: ML_COMPILER =
    6.15  struct
    6.16  
    6.17 -type flags = {SML: bool, verbose: bool};
    6.18 +type flags = {SML: bool, redirect: bool, verbose: bool};
    6.19 +val flags = {SML = false, redirect = false, verbose = false};
    6.20 +fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
    6.21  
    6.22 -fun eval {SML, verbose} pos toks =
    6.23 +fun eval (flags: flags) pos toks =
    6.24    let
    6.25 -    val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
    6.26 +    val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
    6.27      val line = the_default 1 (Position.line_of pos);
    6.28      val file = the_default "ML" (Position.file_of pos);
    6.29      val text = ML_Lex.flatten toks;
    6.30 -  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
    6.31 +  in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end;
    6.32  
    6.33  end;
    6.34  

     7.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
     7.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:56:13 2014 +0100
     7.3 @@ -12,42 +12,65 @@
     7.4  
     7.5  (* parse trees *)
     7.6  
     7.7 -fun report_parse_tree depth space =
     7.8 +fun report_parse_tree redirect depth space parse_tree =
     7.9    let
    7.10 -    val reported_text =
    7.11 +    val is_visible =
    7.12        (case Context.thread_data () of
    7.13 -        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
    7.14 -      | _ => Position.reported_text);
    7.15 +        SOME context => Context_Position.is_visible_generic context
    7.16 +      | NONE => true);
    7.17 +    fun is_reported pos = is_visible andalso Position.is_reported pos;
    7.18 +
    7.19 +    fun reported_types loc types =
    7.20 +      let val pos = Exn_Properties.position_of loc in
    7.21 +        is_reported pos ?
    7.22 +          let
    7.23 +            val xml =
    7.24 +              PolyML.NameSpace.displayTypeExpression (types, depth, space)
    7.25 +              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    7.26 +              |> Output.output |> YXML.parse_body;
    7.27 +          in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
    7.28 +      end;
    7.29  
    7.30      fun reported_entity kind loc decl =
    7.31 -      reported_text (Exn_Properties.position_of loc)
    7.32 -        (Markup.entityN,
    7.33 -          (Markup.kindN, kind) :: Position.def_properties_of (Exn_Properties.position_of decl)) "";
    7.34 +      let val pos = Exn_Properties.position_of loc in
    7.35 +        is_reported pos ?
    7.36 +          let
    7.37 +            val def_pos = Exn_Properties.position_of decl;
    7.38 +            fun markup () =
    7.39 +              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
    7.40 +          in cons (pos, markup, fn () => "") end
    7.41 +      end;
    7.42  
    7.43 -    fun reported loc (PolyML.PTtype types) =
    7.44 -          cons
    7.45 -            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
    7.46 -              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    7.47 -              |> reported_text (Exn_Properties.position_of loc) Markup.ML_typing)
    7.48 -      | reported loc (PolyML.PTdeclaredAt decl) =
    7.49 -          cons (reported_entity Markup.ML_defN loc decl)
    7.50 -      | reported loc (PolyML.PTopenedAt decl) =
    7.51 -          cons (reported_entity Markup.ML_openN loc decl)
    7.52 -      | reported loc (PolyML.PTstructureAt decl) =
    7.53 -          cons (reported_entity Markup.ML_structureN loc decl)
    7.54 +    fun reported loc (PolyML.PTtype types) = reported_types loc types
    7.55 +      | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
    7.56 +      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
    7.57 +      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
    7.58        | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    7.59        | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    7.60        | reported _ _ = I
    7.61      and reported_tree (loc, props) = fold (reported loc) props;
    7.62 -  in fn tree => Output.report (implode (reported_tree tree [])) end;
    7.63 +
    7.64 +    val persistent_reports = reported_tree parse_tree [];
    7.65 +
    7.66 +    fun output () =
    7.67 +      persistent_reports
    7.68 +      |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
    7.69 +      |> implode |> Output.report;
    7.70 +  in
    7.71 +    if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
    7.72 +    then
    7.73 +      Execution.print {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1}
    7.74 +        (fn _ => output ())
    7.75 +    else output ()
    7.76 +  end;
    7.77  
    7.78  
    7.79  (* eval ML source tokens *)
    7.80  
    7.81 -fun eval {SML, verbose} pos toks =
    7.82 +fun eval (flags: flags) pos toks =
    7.83    let
    7.84      val _ = Secure.secure_mltext ();
    7.85 -    val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
    7.86 +    val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space;
    7.87      val opt_context = Context.thread_data ();
    7.88  
    7.89  
    7.90 @@ -133,7 +156,7 @@
    7.91      fun result_fun (phase1, phase2) () =
    7.92       ((case phase1 of
    7.93          NONE => ()
    7.94 -      | SOME parse_tree => report_parse_tree depth space parse_tree);
    7.95 +      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
    7.96        (case phase2 of
    7.97          NONE => raise STATIC_ERRORS ()
    7.98        | SOME code =>
    7.99 @@ -171,7 +194,7 @@
   7.100              val _ = output_writeln ();
   7.101            in raise_error exn_msg end;
   7.102    in
   7.103 -    if verbose then (output_warnings (); flush_error (); output_writeln ())
   7.104 +    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
   7.105      else ()
   7.106    end;
   7.107  

     8.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 27 17:12:40 2014 +0100
     8.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 27 17:56:13 2014 +0100
     8.3 @@ -137,7 +137,7 @@
     8.4  
     8.5  fun eval flags pos ants =
     8.6    let
     8.7 -    val non_verbose = {SML = #SML flags, verbose = false};
     8.8 +    val non_verbose = ML_Compiler.verbose false flags;
     8.9  
    8.10      (*prepare source text*)
    8.11      val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
    8.12 @@ -181,13 +181,14 @@
    8.13      (fn () => eval_source flags source) ();
    8.14  
    8.15  fun expression pos bind body ants =
    8.16 -  exec (fn () => eval {SML = false, verbose = false} pos
    8.17 -    (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
    8.18 +  exec (fn () =>
    8.19 +    eval ML_Compiler.flags pos
    8.20 +     (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
    8.21        ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
    8.22  
    8.23  end;
    8.24  
    8.25  fun use s =
    8.26 -  ML_Context.eval_file {SML = false, verbose = true} (Path.explode s)
    8.27 +  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
    8.28      handle ERROR msg => (writeln msg; error "ML error");
    8.29  

     9.1 --- a/src/Pure/ML/ml_thms.ML	Thu Mar 27 17:12:40 2014 +0100
     9.2 +++ b/src/Pure/ML/ml_thms.ML	Thu Mar 27 17:56:13 2014 +0100
     9.3 @@ -130,7 +130,7 @@
     9.4        else if not (ML_Syntax.is_identifier name) then
     9.5          error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
     9.6        else
     9.7 -        ML_Compiler.eval {SML = false, verbose = true} Position.none
     9.8 +        ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
     9.9            (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
    9.10      val _ = Theory.setup (Stored_Thms.put []);
    9.11    in () end;

    10.1 --- a/src/Pure/PIDE/execution.ML	Thu Mar 27 17:12:40 2014 +0100
    10.2 +++ b/src/Pure/PIDE/execution.ML	Thu Mar 27 17:56:13 2014 +0100
    10.3 @@ -18,7 +18,6 @@
    10.4    type params = {name: string, pos: Position.T, pri: int}
    10.5    val fork: params -> (unit -> 'a) -> 'a future
    10.6    val print: params -> (serial -> unit) -> unit
    10.7 -  val print_report: string -> unit
    10.8    val fork_prints: Document_ID.exec -> unit
    10.9    val purge: Document_ID.exec list -> unit
   10.10    val reset: unit -> Future.group list
   10.11 @@ -148,14 +147,6 @@
   10.12        | NONE => raise Fail (unregistered exec_id))
   10.13      end));
   10.14  
   10.15 -fun print_report s =
   10.16 -  if s = "" orelse not (Multithreading.enabled ()) then Output.direct_report s
   10.17 -  else
   10.18 -    let
   10.19 -      val body = YXML.parse_body s  (*sharable closure!*)
   10.20 -      val params = {name = "", pos = Position.thread_data (), pri = 0};
   10.21 -    in print params (fn _ => Output.direct_report (YXML.string_of_body body)) end;
   10.22 -
   10.23  fun fork_prints exec_id =
   10.24    (case Inttab.lookup (#2 (get_state ())) exec_id of
   10.25      SOME (_, prints) =>

    11.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 27 17:12:40 2014 +0100
    11.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Mar 27 17:56:13 2014 +0100
    11.3 @@ -639,7 +639,7 @@
    11.4  
    11.5  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
    11.6    (fn {context, ...} => fn source =>
    11.7 -   (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
    11.8 +   (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
    11.9      Symbol_Pos.source_content source
   11.10      |> #1
   11.11      |> (if Config.get context quotes then quote else I)

    12.1 --- a/src/Pure/pure_syn.ML	Thu Mar 27 17:12:40 2014 +0100
    12.2 +++ b/src/Pure/pure_syn.ML	Thu Mar 27 17:56:13 2014 +0100
    12.3 @@ -23,9 +23,10 @@
    12.4            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    12.5            val provide = Resources.provide (src_path, digest);
    12.6            val source = {delimited = true, text = cat_lines lines, pos = pos};
    12.7 +          val flags = {SML = false, redirect = true, verbose = true};
    12.8          in
    12.9            gthy
   12.10 -          |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source)
   12.11 +          |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
   12.12            |> Local_Theory.propagate_ml_env
   12.13            |> Context.mapping provide (Local_Theory.background_theory provide)
   12.14          end)));