restore output channels after shutdown, e.g. relevant for saved heap;
--- a/src/Pure/General/output.ML Sat Mar 18 12:24:56 2017 +0100
+++ b/src/Pure/General/output.ML Sat Mar 18 12:46:52 2017 +0100
@@ -57,6 +57,7 @@
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
+ val init_channels: unit -> unit
end;
structure Private_Output: PRIVATE_OUTPUT =
@@ -119,17 +120,21 @@
exception Protocol_Message of Properties.T;
-val _ =
- if Thread_Data.is_virtual then ()
- else
- (writeln_fn := (physical_writeln o implode);
- state_fn := (fn ss => ! writeln_fn ss);
- tracing_fn := (fn ss => ! writeln_fn ss);
- warning_fn := (physical_writeln o prefix_lines "### " o implode);
- legacy_fn := (fn ss => ! warning_fn ss);
- error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
- system_message_fn := (fn ss => ! writeln_fn ss);
- protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
+fun init_channels () =
+ (writeln_fn := (physical_writeln o implode);
+ state_fn := (fn ss => ! writeln_fn ss);
+ information_fn := Output_Primitives.ignore_outputs;
+ tracing_fn := (fn ss => ! writeln_fn ss);
+ warning_fn := (physical_writeln o prefix_lines "### " o implode);
+ legacy_fn := (fn ss => ! warning_fn ss);
+ error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
+ system_message_fn := (fn ss => ! writeln_fn ss);
+ status_fn := Output_Primitives.ignore_outputs;
+ report_fn := Output_Primitives.ignore_outputs;
+ result_fn := (fn _ => Output_Primitives.ignore_outputs);
+ protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
+
+val _ = if Thread_Data.is_virtual then () else init_channels ();
fun writelns ss = ! writeln_fn (map output ss);
fun writeln s = writelns [s];
--- a/src/Pure/General/output_primitives.ML Sat Mar 18 12:24:56 2017 +0100
+++ b/src/Pure/General/output_primitives.ML Sat Mar 18 12:46:52 2017 +0100
@@ -9,6 +9,7 @@
type output = string
type serial = int
type properties = (string * string) list
+ val ignore_outputs: output list -> unit
val writeln_fn: output list -> unit
val state_fn: output list -> unit
val information_fn: output list -> unit
--- a/src/Pure/System/isabelle_process.ML Sat Mar 18 12:24:56 2017 +0100
+++ b/src/Pure/System/isabelle_process.ML Sat Mar 18 12:46:52 2017 +0100
@@ -205,7 +205,9 @@
val channel = System_Channel.rendezvous socket;
val msg_channel = init_channels channel;
val _ = loop channel;
- in Message_Channel.shutdown msg_channel end);
+ val _ = Message_Channel.shutdown msg_channel;
+ val _ = Private_Output.init_channels ();
+ in () end);
(* init options *)