more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);

--- a/src/Pure/General/output.ML	Mon Mar 30 19:50:01 2020 +0200
+++ b/src/Pure/General/output.ML	Tue Mar 31 14:09:36 2020 +0200
@@ -59,7 +59,6 @@
   val report_fn: (output list -> unit) Unsynchronized.ref
   val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
   val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref
-  val init_channels: unit -> unit
 end;
 
 structure Private_Output: PRIVATE_OUTPUT =

--- a/src/Pure/System/isabelle_process.ML	Mon Mar 30 19:50:01 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Mar 31 14:09:36 2020 +0200
@@ -28,6 +28,9 @@
 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
 
+val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
+val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
+
 
 (* protocol commands *)
 
@@ -92,16 +95,43 @@
       end);
 
 
-(* output channels *)
+(* init protocol -- uninterruptible *)
+
+exception EXIT of exn;
+
+val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
+
+local
+
+fun recover crash =
+  (Synchronized.change crashes (cons crash);
+    Output.physical_stderr
+      "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
+
+in
 
-val serial_props = Markup.serial_properties o serial;
+val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
+  let
+    val _ = SHA1.test_samples ()
+      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
+
+    val _ = Output.physical_stderr Symbol.STX;
 
-fun init_channels out_stream =
-  let
+    val _ = Context.put_generic_context NONE;
+
+
+    (* streams *)
+
+    val (in_stream, out_stream) = Socket_IO.open_streams address;
+    val _ = Byte_Message.write_line out_stream password;
+
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
     val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
 
+
+    (* messages *)
+
     val msg_channel = Message_Channel.make out_stream;
 
     fun message name props body =
@@ -116,90 +146,70 @@
               (false, SOME id') => props @ [(Markup.idN, id')]
             | _ => props);
         in message name props' (XML.blob ss) end;
-  in
-    Private_Output.status_fn := standard_message [] Markup.statusN;
-    Private_Output.report_fn := standard_message [] Markup.reportN;
-    Private_Output.result_fn :=
-      (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
-    Private_Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
-    Private_Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s);
-    Private_Output.information_fn :=
-      (fn s => standard_message (serial_props ()) Markup.informationN s);
-    Private_Output.tracing_fn :=
-      (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
-    Private_Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
-    Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
-    Private_Output.error_message_fn :=
-      (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
-    Private_Output.system_message_fn :=
-      (fn ss => message Markup.systemN [] (XML.blob ss));
-    Private_Output.protocol_message_fn :=
-      (fn props => fn body => message Markup.protocolN props body);
+
+    val serial_props = Markup.serial_properties o serial;
 
-    Session.init_protocol_handlers ();
-    message Markup.initN [] [XML.Text (Session.welcome ())];
-    msg_channel
-  end;
+    val message_context =
+      Unsynchronized.setmp Private_Output.status_fn
+        (standard_message [] Markup.statusN) #>
+      Unsynchronized.setmp Private_Output.report_fn
+        (standard_message [] Markup.reportN) #>
+      Unsynchronized.setmp Private_Output.result_fn
+        (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
+      Unsynchronized.setmp Private_Output.writeln_fn
+        (fn s => standard_message (serial_props ()) Markup.writelnN s) #>
+      Unsynchronized.setmp Private_Output.state_fn
+        (fn s => standard_message (serial_props ()) Markup.stateN s) #>
+      Unsynchronized.setmp Private_Output.information_fn
+        (fn s => standard_message (serial_props ()) Markup.informationN s) #>
+      Unsynchronized.setmp Private_Output.tracing_fn
+        (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #>
+      Unsynchronized.setmp Private_Output.warning_fn
+        (fn s => standard_message (serial_props ()) Markup.warningN s) #>
+      Unsynchronized.setmp Private_Output.legacy_fn
+        (fn s => standard_message (serial_props ()) Markup.legacyN s) #>
+      Unsynchronized.setmp Private_Output.error_message_fn
+        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #>
+      Unsynchronized.setmp Private_Output.system_message_fn
+        (fn ss => message Markup.systemN [] (XML.blob ss)) #>
+      Unsynchronized.setmp Private_Output.protocol_message_fn
+        (fn props => fn body => message Markup.protocolN props body) #>
+      Unsynchronized.setmp print_mode
+        ((! print_mode @ protocol_modes1) |> fold (update op =) protocol_modes2);
 
 
-(* protocol loop -- uninterruptible *)
-
-exception EXIT of exn;
-
-val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
+    (* protocol *)
 
-local
-
-fun recover crash =
-  (Synchronized.change crashes (cons crash);
-    Output.physical_stderr
-      "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
+    fun protocol_loop () =
+      let
+        val continue =
+          (case Byte_Message.read_message in_stream of
+            NONE => false
+          | SOME [] => (Output.system_message "Isabelle process: no input"; true)
+          | SOME (name :: args) => (run_command name args; true))
+          handle EXIT exn => Exn.reraise exn
+            | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
+      in if continue then protocol_loop () else () end;
 
-fun shutdown () = (Future.shutdown (); ignore (Execution.reset ()));
+    fun protocol () =
+     (Session.init_protocol_handlers ();
+      message Markup.initN [] [XML.Text (Session.welcome ())];
+      protocol_loop ());
 
-in
+    val result = Exn.capture (message_context protocol) ();
+
 
-fun loop stream =
-  let
-    val continue =
-      (case Byte_Message.read_message stream of
-        NONE => false
-      | SOME [] => (Output.system_message "Isabelle process: no input"; true)
-      | SOME (name :: args) => (run_command name args; true))
-      handle EXIT exn => (shutdown (); Exn.reraise exn)
-        | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
-  in if continue then loop stream else shutdown () end;
+    (* shutdown *)
+
+    val _ = Future.shutdown ();
+    val _ = Execution.reset ();
+    val _ = Message_Channel.shutdown msg_channel;
+
+  in Exn.release result end);
 
 end;
 
 
-(* init protocol *)
-
-val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
-val default_modes2 = [isabelle_processN, Pretty.symbolicN];
-
-val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
-  let
-    val _ = SHA1.test_samples ()
-      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
-    val _ = Output.physical_stderr Symbol.STX;
-
-    val _ = Context.put_generic_context NONE;
-    val _ =
-      Unsynchronized.change print_mode
-        (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
-
-    val (in_stream, out_stream) = Socket_IO.open_streams address;
-    val _ = Byte_Message.write_line out_stream password;
-    val msg_channel = init_channels out_stream;
-    val _ = loop in_stream;
-    val _ = Message_Channel.shutdown msg_channel;
-    val _ = Private_Output.init_channels ();
-
-    val _ = print_mode := [];
-  in () end);
-
-
 (* init options *)
 
 fun init_options () =