proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;

--- a/src/Pure/PIDE/session.scala	Thu Apr 02 13:04:24 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 02 20:06:43 2020 +0200
@@ -705,22 +705,17 @@
       })
   }
 
-  def send_stop()
+  def stop(): Process_Result =
   {
     val was_ready =
-      _phase.guarded_access(phase =>
-        phase match {
+      _phase.guarded_access(
+        {
           case Session.Startup | Session.Shutdown => None
           case Session.Terminated(_) => Some((false, phase))
           case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
         })
     if (was_ready) manager.send(Stop)
-  }
-
-  def stop(): Process_Result =
-  {
-    send_stop()
     prover.await_reset()
 
     change_parser.shutdown()

--- a/src/Pure/System/isabelle_process.ML	Thu Apr 02 13:04:24 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Thu Apr 02 20:06:43 2020 +0200
@@ -7,9 +7,10 @@
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
+  exception STOP
+  exception EXIT of int
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
-  exception EXIT of int
   val crashes: exn list Synchronized.var
   val init_options: unit -> unit
   val init_options_interactive: unit -> unit
@@ -35,6 +36,11 @@
 
 (* protocol commands *)
 
+exception STOP;
+exception EXIT of int;
+
+val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false;
+
 local
 
 val commands =
@@ -54,7 +60,9 @@
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
       (Runtime.exn_trace_system (fn () => cmd args)
-        handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name)));
+        handle exn =>
+          if is_protocol_exn exn then Exn.reraise exn
+          else error ("Isabelle protocol command failure: " ^ quote name)));
 
 end;
 
@@ -98,8 +106,6 @@
 
 (* init protocol -- uninterruptible *)
 
-exception EXIT of int;
-
 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
 local
@@ -181,14 +187,15 @@
 
     fun protocol_loop () =
       let
-        val continue =
+        val _ =
           (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 exn as EXIT _ => Exn.reraise exn
-            | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
-      in if continue then protocol_loop () else () end;
+            NONE => raise STOP
+          | SOME [] => Output.system_message "Isabelle process: no input"
+          | SOME (name :: args) => run_command name args)
+          handle exn =>
+            if is_protocol_exn exn then Exn.reraise exn
+            else (Runtime.exn_system_message exn handle crash => recover crash);
+      in protocol_loop () end;
 
     fun protocol () =
      (Session.init_protocol_handlers ();
@@ -205,9 +212,11 @@
     val _ = Message_Channel.shutdown msg_channel;
     val _ = BinIO.closeIn in_stream;
     val _ = BinIO.closeOut out_stream;
+
   in
     (case result of
-      Exn.Exn (EXIT rc) => exit rc
+      Exn.Exn STOP => ()
+    | Exn.Exn (EXIT rc) => exit rc
     | _ => Exn.release result)
   end);
 

--- a/src/Pure/System/isabelle_process.scala	Thu Apr 02 13:04:24 2020 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Apr 02 20:06:43 2020 +0200
@@ -70,5 +70,10 @@
       case err => session.stop(); error(err)
     }
 
-  def join(): Process_Result = terminated.join
-}
\ No newline at end of file
+  def await_shutdown(): Process_Result =
+  {
+    val result = terminated.join
+    session.stop()
+    result
+  }
+}

--- a/src/Pure/Tools/build.ML	Thu Apr 02 13:04:24 2020 +0200
+++ b/src/Pure/Tools/build.ML	Thu Apr 02 20:06:43 2020 +0200
@@ -254,13 +254,16 @@
         let
           val args = decode_args args_yxml;
           val errs =
-            Future.interruptible_task (fn () =>
-              (build_session args; []) handle exn =>
+            Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
               (Runtime.exn_message_list exn handle _ (*sic!*) =>
                 (build_session_finished ["CRASHED"];
-                  raise Isabelle_Process.EXIT 1))) ();
+                  raise Isabelle_Process.EXIT 2));
           val _ = build_session_finished errs;
-        in if null errs then () else raise Isabelle_Process.EXIT 1 end
+        in
+          if null errs
+          then raise Isabelle_Process.STOP
+          else raise Isabelle_Process.EXIT 1
+        end
       | _ => raise Match);
 
 end;

--- a/src/Pure/Tools/build.scala	Thu Apr 02 13:04:24 2020 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 02 20:06:43 2020 +0200
@@ -166,7 +166,6 @@
         }
         catch { case ERROR(err) => List(err) }
       build_session_errors.fulfill(errors)
-      session.send_stop()
       true
     }
 
@@ -297,8 +296,9 @@
               cwd = info.dir.file, env = env).await_startup
 
           session.protocol_command("build_session", args_yxml)
+          val errors = handler.build_session_errors.join
 
-          val process_result = process.join
+          val process_result = process.await_shutdown
           val process_output =
             stdout.toString :: messages.toList :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
@@ -307,12 +307,11 @@
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
 
           val result = process_result.output(process_output)
-          handler.build_session_errors.join match {
-            case Nil => result
-            case errors =>
-              result.error_rc.output(
-                errors.flatMap(s => split_lines(Output.error_message_text(s))) :::
-                errors.map(Protocol.Error_Message_Marker.apply))
+          if (errors.isEmpty) result
+          else {
+            result.error_rc.output(
+              errors.flatMap(s => split_lines(Output.error_message_text(s))) :::
+              errors.map(Protocol.Error_Message_Marker.apply))
           }
         }
         else {