support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Mar 31 10:28:08 2014 +0200
@@ -505,6 +505,6 @@
let
val this_thy = @{theory}
val provers = space_implode " " (#provers (default_params this_thy []))
- in Output.protocol_message Markup.sledgehammer_provers provers end)
+ in Output.protocol_message Markup.sledgehammer_provers [provers] end)
end;
--- a/src/Pure/Concurrent/future.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Mar 31 10:28:08 2014 +0200
@@ -56,7 +56,7 @@
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> unit
val cancel: 'a future -> unit
- val error_msg: Position.T -> (serial * string) * string option -> unit
+ val error_message: Position.T -> (serial * string) * string option -> unit
val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
val default_params: params
@@ -210,7 +210,7 @@
("workers_active", Markup.print_int active),
("workers_waiting", Markup.print_int waiting)] @
ML_Statistics.get ();
- in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end
+ in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
else ();
@@ -257,7 +257,7 @@
fold (fn job => fn ok => job valid andalso ok) jobs true) ());
val _ =
if ! Multithreading.trace >= 2 then
- Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
+ Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) []
else ();
val _ = SYNCHRONIZED "finish" (fn () =>
let
@@ -434,7 +434,7 @@
(* results *)
-fun error_msg pos ((serial, msg), exec_id) =
+fun error_message pos ((serial, msg), exec_id) =
Position.setmp_thread_data pos (fn () =>
let val id = Position.get_id pos in
if is_none id orelse is_none exec_id orelse id = exec_id
--- a/src/Pure/General/output.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/General/output.ML Mon Mar 31 10:28:08 2014 +0200
@@ -30,25 +30,25 @@
val error_message: string -> unit
val prompt: string -> unit
val status: string -> unit
- val report: string -> unit
- val result: Properties.T -> string -> unit
- val protocol_message: Properties.T -> string -> unit
- val try_protocol_message: Properties.T -> string -> unit
+ val report: string list -> unit
+ val result: Properties.T -> string list -> unit
+ val protocol_message: Properties.T -> string list -> unit
+ val try_protocol_message: Properties.T -> string list -> unit
end;
signature PRIVATE_OUTPUT =
sig
include OUTPUT
- val writeln_fn: (output -> unit) Unsynchronized.ref
- val urgent_message_fn: (output -> unit) Unsynchronized.ref
- val tracing_fn: (output -> unit) Unsynchronized.ref
- val warning_fn: (output -> unit) Unsynchronized.ref
- val error_message_fn: (serial * output -> unit) Unsynchronized.ref
+ val writeln_fn: (output list -> unit) Unsynchronized.ref
+ val urgent_message_fn: (output list -> unit) Unsynchronized.ref
+ val tracing_fn: (output list -> unit) Unsynchronized.ref
+ val warning_fn: (output list -> unit) Unsynchronized.ref
+ val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
val prompt_fn: (output -> unit) Unsynchronized.ref
- val status_fn: (output -> unit) Unsynchronized.ref
- val report_fn: (output -> unit) Unsynchronized.ref
- val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
- val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+ val status_fn: (output list -> unit) Unsynchronized.ref
+ val report_fn: (output list -> unit) Unsynchronized.ref
+ val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
+ val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
end;
structure Output: PRIVATE_OUTPUT =
@@ -94,31 +94,31 @@
exception Protocol_Message of Properties.T;
-val writeln_fn = Unsynchronized.ref physical_writeln;
-val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*)
-val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
+val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
+val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); (*Proof General legacy*)
+val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
+val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
val error_message_fn =
- Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
-val prompt_fn = Unsynchronized.ref physical_stdout;
-val status_fn = Unsynchronized.ref (fn _: output => ());
-val report_fn = Unsynchronized.ref (fn _: output => ());
-val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
-val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+ Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
+val prompt_fn = Unsynchronized.ref physical_stdout; (*Proof General legacy*)
+val status_fn = Unsynchronized.ref (fn _: output list => ());
+val report_fn = Unsynchronized.ref (fn _: output list => ());
+val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
+val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
-fun writeln s = ! writeln_fn (output s);
-fun urgent_message s = ! urgent_message_fn (output s); (*Proof General legacy*)
-fun tracing s = ! tracing_fn (output s);
-fun warning s = ! warning_fn (output s);
-fun error_message' (i, s) = ! error_message_fn (i, output s);
+fun writeln s = ! writeln_fn [output s];
+fun urgent_message s = ! urgent_message_fn [output s]; (*Proof General legacy*)
+fun tracing s = ! tracing_fn [output s];
+fun warning s = ! warning_fn [output s];
+fun error_message' (i, s) = ! error_message_fn (i, [output s]);
fun error_message s = error_message' (serial (), s);
fun prompt s = ! prompt_fn (output s);
-fun status s = ! status_fn (output s);
-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 _ => ();
+fun status s = ! status_fn [output s];
+fun report ss = ! report_fn (map output ss);
+fun result props ss = ! result_fn props (map output ss);
+fun protocol_message props ss = ! protocol_message_fn props (map output ss);
+fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
end;
--- a/src/Pure/General/position.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/General/position.ML Mon Mar 31 10:28:08 2014 +0200
@@ -166,7 +166,7 @@
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
-fun report_text pos markup txt = Output.report (reported_text pos markup txt);
+fun report_text pos markup txt = Output.report [reported_text pos markup txt];
fun report pos markup = report_text pos markup "";
type report = T * Markup.T;
@@ -174,7 +174,7 @@
val reports_text =
map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
- #> implode #> Output.report;
+ #> Output.report;
val reports = map (rpair "") #> reports_text;
--- a/src/Pure/General/timing.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/General/timing.ML Mon Mar 31 10:28:08 2014 +0200
@@ -105,7 +105,7 @@
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
fun protocol_message props t =
- Output.try_protocol_message (props @ Markup.timing_properties t) "";
+ Output.try_protocol_message (props @ Markup.timing_properties t) [];
fun protocol props f x =
let
--- a/src/Pure/Isar/args.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Isar/args.ML Mon Mar 31 10:28:08 2014 +0200
@@ -277,8 +277,7 @@
if Context_Position.is_visible_generic context then
((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1)
|> map (fn (p, m) => Position.reported_text p m "")
- |> implode
- else "";
+ else [];
in
(case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
(SOME x, (context', [])) =>
@@ -294,7 +293,7 @@
if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2);
in
error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
- Markup.markup_report (reported_text ()))
+ Markup.markup_report (implode (reported_text ())))
end)
end;
--- a/src/Pure/Isar/isar_syn.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Mar 31 10:28:08 2014 +0200
@@ -716,7 +716,7 @@
(* proof navigation *)
fun report_back () =
- Output.report (Markup.markup Markup.bad "Explicit backtracking");
+ Output.report [Markup.markup Markup.bad "Explicit backtracking"];
val _ =
Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
--- a/src/Pure/Isar/proof_context.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 31 10:28:08 2014 +0200
@@ -78,8 +78,8 @@
val read_arity: Proof.context -> xstring * string list * string -> arity
val cert_arity: Proof.context -> arity -> arity
val allow_dummies: Proof.context -> Proof.context
- val prepare_sortsT: Proof.context -> typ list -> string * typ list
- val prepare_sorts: Proof.context -> term list -> string * term list
+ val prepare_sortsT: Proof.context -> typ list -> string list * typ list
+ val prepare_sorts: Proof.context -> term list -> string list * term list
val check_tfree: Proof.context -> string * sort -> string * sort
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
@@ -691,7 +691,7 @@
| TVar (xi, raw_S) => get_sort_reports xi raw_S
| _ => I)) tys [];
- in (implode (map #2 reports), get_sort) end;
+ in (map #2 reports, get_sort) end;
fun replace_sortsT get_sort =
map_atyps
--- a/src/Pure/ML/ml_compiler_polyml.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Mar 31 10:28:08 2014 +0200
@@ -55,7 +55,7 @@
fun output () =
persistent_reports
|> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
- |> implode |> Output.report;
+ |> Output.report;
in
if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
then
--- a/src/Pure/PIDE/command.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/PIDE/command.ML Mon Mar 31 10:28:08 2014 +0200
@@ -199,7 +199,7 @@
else Runtime.exn_messages_ids exn)) ();
fun report tr m =
- Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
+ Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
fun status tr m =
Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
@@ -223,7 +223,7 @@
val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
val errs = errs1 @ errs2;
- val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
+ val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
in
(case result of
NONE =>
@@ -279,7 +279,7 @@
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
handle exn =>
if Exn.is_interrupt exn then reraise exn
- else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
+ else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
fun print_finished (Print {print_process, ...}) = memo_finished print_process;
--- a/src/Pure/PIDE/execution.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/PIDE/execution.ML Mon Mar 31 10:28:08 2014 +0200
@@ -122,9 +122,9 @@
Exn.Exn exn =>
(status task [Markup.failed];
status task [Markup.finished];
- Output.report (Markup.markup_only Markup.bad);
+ Output.report [Markup.markup_only Markup.bad];
if exec_id = 0 then ()
- else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
+ else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
| Exn.Res _ =>
status task [Markup.finished])
in Exn.release result end);
--- a/src/Pure/PIDE/protocol.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Mar 31 10:28:08 2014 +0200
@@ -85,10 +85,10 @@
val _ =
Output.protocol_message Markup.assign_update
- ((new_id, assign_update) |>
+ [(new_id, assign_update) |>
let open XML.Encode
in pair int (list (pair int (list int))) end
- |> YXML.string_of_body);
+ |> YXML.string_of_body];
in Document.start_execution state' end));
val _ =
@@ -99,7 +99,7 @@
YXML.parse_body versions_yxml |>
let open XML.Decode in list int end;
val state1 = Document.remove_versions versions state;
- val _ = Output.protocol_message Markup.removed_versions versions_yxml;
+ val _ = Output.protocol_message Markup.removed_versions [versions_yxml];
in state1 end));
val _ =
--- a/src/Pure/PIDE/query_operation.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Mar 31 10:28:08 2014 +0200
@@ -20,7 +20,7 @@
SOME {delay = NONE, pri = 0, persistent = false, strict = false,
print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
let
- fun result s = Output.result [(Markup.instanceN, instance)] s;
+ fun result s = Output.result [(Markup.instanceN, instance)] [s];
fun status m = result (Markup.markup_only m);
fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
fun toplevel_error exn =
--- a/src/Pure/PIDE/resources.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/PIDE/resources.ML Mon Mar 31 10:28:08 2014 +0200
@@ -213,7 +213,7 @@
if strict then error msg
else if Context_Position.is_visible ctxt then
Output.report
- (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
+ [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg]
else ()
end;
in path end;
--- a/src/Pure/PIDE/session.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/PIDE/session.ML Mon Mar 31 10:28:08 2014 +0200
@@ -68,13 +68,13 @@
fun protocol_handler name =
Synchronized.change protocol_handlers (fn handlers =>
- (Output.try_protocol_message (Markup.protocol_handler name) "";
+ (Output.try_protocol_message (Markup.protocol_handler name) [];
if not (member (op =) handlers name) then ()
else warning ("Redefining protocol handler: " ^ quote name);
update (op =) name handlers));
fun init_protocol_handlers () =
Synchronized.value protocol_handlers
- |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
+ |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
end;
--- a/src/Pure/Syntax/syntax_phases.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Mar 31 10:28:08 2014 +0200
@@ -949,11 +949,10 @@
if Position.is_reported pos then
cons (Position.reported_text pos Markup.typing
(Syntax.string_of_typ ctxt (Logic.dest_type ty)))
- else I) ps tys' []
- |> implode;
+ else I) ps tys' [];
val _ =
- if Context_Position.is_visible ctxt then Output.report (sorting_report ^ typing_report)
+ if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report)
else ();
in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
--- a/src/Pure/System/invoke_scala.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/System/invoke_scala.ML Mon Mar 31 10:28:08 2014 +0200
@@ -30,10 +30,10 @@
fun promise_method name arg =
let
val id = new_id ();
- fun abort () = Output.protocol_message (Markup.cancel_scala id) "";
+ fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
val promise = Future.promise abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
- val _ = Output.protocol_message (Markup.invoke_scala name id) arg;
+ val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
in promise end;
fun method name arg = Future.join (promise_method name arg);
--- a/src/Pure/System/isabelle_process.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Mar 31 10:28:08 2014 +0200
@@ -106,7 +106,7 @@
Message_Channel.send msg_channel (Message_Channel.message name props body);
fun standard_message props name body =
- if body = "" then ()
+ if forall (fn s => s = "") body then ()
else
message name
(fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
@@ -124,7 +124,7 @@
Output.protocol_message_fn := message Markup.protocolN;
Output.urgent_message_fn := ! Output.writeln_fn;
Output.prompt_fn := ignore;
- message Markup.initN [] (Session.welcome ());
+ message Markup.initN [] [Session.welcome ()];
msg_channel
end;
--- a/src/Pure/System/message_channel.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/System/message_channel.ML Mon Mar 31 10:28:08 2014 +0200
@@ -7,7 +7,7 @@
signature MESSAGE_CHANNEL =
sig
type message
- val message: string -> Properties.T -> string -> message
+ val message: string -> Properties.T -> string list -> message
type T
val send: T -> message -> unit
val shutdown: T -> unit
@@ -21,13 +21,14 @@
datatype message = Message of string list;
-fun chunk s = [string_of_int (size s), "\n", s];
+fun chunk ss =
+ string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
fun message name raw_props body =
let
val robust_props = map (pairself YXML.embed_controls) raw_props;
val header = YXML.string_of (XML.Elem ((name, robust_props), []));
- in Message (chunk header @ chunk body) end;
+ in Message (chunk [header] @ chunk body) end;
fun output_message channel (Message ss) =
List.app (System_Channel.output channel) ss;
@@ -37,7 +38,7 @@
fun flush channel = ignore (try System_Channel.flush channel);
-val flush_message = message Markup.protocolN Markup.flush "";
+val flush_message = message Markup.protocolN Markup.flush [];
fun flush_output channel = (output_message channel flush_message; flush channel);
--- a/src/Pure/Thy/thy_info.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Mar 31 10:28:08 2014 +0200
@@ -269,7 +269,7 @@
let
val _ = kill_thy name;
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
- val _ = Output.try_protocol_message (Markup.loading_theory name) "";
+ val _ = Output.try_protocol_message (Markup.loading_theory name) [];
val {master = (thy_path, _), imports} = deps;
val dir = Path.dir thy_path;
--- a/src/Pure/Tools/proof_general.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Tools/proof_general.ML Mon Mar 31 10:28:08 2014 +0200
@@ -258,8 +258,8 @@
(* hooks *)
-fun message bg en prfx text =
- (case render text of
+fun message bg en prfx body =
+ (case render (implode body) of
"" => ()
| s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
@@ -276,7 +276,7 @@
(* notification *)
-val emacs_notify = message (special "I") (special "J") "";
+fun emacs_notify s = message (special "I") (special "J") "" [s];
fun tell_clear_goals () =
emacs_notify "Proof General, please clear the goals buffer.";
--- a/src/Pure/Tools/simplifier_trace.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Mon Mar 31 10:28:08 2014 +0200
@@ -133,7 +133,7 @@
(** markup **)
fun output_result (id, data) =
- Output.result (Markup.serial_properties id) data
+ Output.result (Markup.serial_properties id) [data]
val parentN = "parent"
val textN = "text"
@@ -184,7 +184,7 @@
fun send_request (result_id, content) =
let
fun break () =
- (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
+ (Output.protocol_message (Markup.simp_trace_cancel result_id) [];
Synchronized.change futures (Inttab.delete_safe result_id))
val promise = Future.promise break : string future
in
--- a/src/Pure/context_position.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/context_position.ML Mon Mar 31 10:28:08 2014 +0200
@@ -49,13 +49,13 @@
fun report_generic context pos markup =
if is_reported_generic context pos then
- Output.report (Position.reported_text pos markup "")
+ Output.report [Position.reported_text pos markup ""]
else ();
fun reported_text ctxt pos markup txt =
if is_reported ctxt pos then Position.reported_text pos markup txt else "";
-fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
+fun report_text ctxt pos markup txt = Output.report [reported_text ctxt pos markup txt];
fun report ctxt pos markup = report_text ctxt pos markup "";
fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else ();
--- a/src/Pure/skip_proof.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/skip_proof.ML Mon Mar 31 10:28:08 2014 +0200
@@ -19,7 +19,7 @@
fun report ctxt =
if Context_Position.is_visible ctxt then
- Output.report (Markup.markup Markup.bad "Skipped proof")
+ Output.report [Markup.markup Markup.bad "Skipped proof"]
else ();