# HG changeset patch
# User wenzelm
# Date 1489837612 -3600
# Node ID fca593a627859eed2d1499f923fac0314a7256ce
# Parent  c262653a3b88b46b268279d880b101011b3fbd49
restore output channels after shutdown, e.g. relevant for saved heap;

diff -r c262653a3b88 -r fca593a62785 src/Pure/General/output.ML
--- 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];
diff -r c262653a3b88 -r fca593a62785 src/Pure/General/output_primitives.ML
--- 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
diff -r c262653a3b88 -r fca593a62785 src/Pure/System/isabelle_process.ML
--- 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 *)