clarified signature;

--- a/src/Pure/System/isabelle_process.ML	Sun May 24 12:43:04 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sun May 24 13:39:45 2020 +0200
@@ -7,8 +7,7 @@
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
-  exception STOP
-  exception EXIT of int
+  exception STOP of int
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
@@ -36,10 +35,9 @@
 
 (* protocol commands *)
 
-exception STOP;
-exception EXIT of int;
+exception STOP of int;
 
-val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false;
+val is_protocol_exn = fn STOP _ => true | _ => false;
 
 local
 
@@ -191,7 +189,7 @@
       let
         val _ =
           (case Byte_Message.read_message in_stream of
-            NONE => raise STOP
+            NONE => raise STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
           | SOME (name :: args) => run_command name args)
           handle exn =>
@@ -217,8 +215,7 @@
 
   in
     (case result of
-      Exn.Exn STOP => ()
-    | Exn.Exn (EXIT rc) => exit rc
+      Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
     | _ => Exn.release result)
   end);
 

--- a/src/Pure/Tools/build.ML	Sun May 24 12:43:04 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 24 13:39:45 2020 +0200
@@ -260,12 +260,12 @@
             Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
               (Runtime.exn_message_list exn handle _ (*sic!*) =>
                 (build_session_finished ["CRASHED"];
-                  raise Isabelle_Process.EXIT 2));
+                  raise Isabelle_Process.STOP 2));
           val _ = build_session_finished errs;
         in
           if null errs
-          then raise Isabelle_Process.STOP
-          else raise Isabelle_Process.EXIT 1
+          then raise Isabelle_Process.STOP 0
+          else raise Isabelle_Process.STOP 1
         end
       | _ => raise Match);