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