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;
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)));