# HG changeset patch
# User wenzelm
# Date 1585824593 -7200
# Node ID 3e121f999120eb6e3f662f1e5adf0359bc99266e
# Parent  dad29591645a47c3d62a7b852a85aa12ca797b4b
clarified signature: more direct Isabelle_Process.EXIT;

diff -r dad29591645a -r 3e121f999120 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Thu Apr 02 12:19:09 2020 +0200
+++ b/src/Pure/System/command_line.ML	Thu Apr 02 12:49:53 2020 +0200
@@ -6,22 +6,18 @@
 
 signature COMMAND_LINE =
 sig
-  exception EXIT of int
   val tool: (unit -> unit) -> unit
 end;
 
 structure Command_Line: COMMAND_LINE =
 struct
 
-exception EXIT of int;
-
 fun tool body =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val rc =
         (restore_attributes body (); 0)
-          handle EXIT rc => rc
-            | exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+          handle exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
     in exit rc end) ();
 
 end;
diff -r dad29591645a -r 3e121f999120 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Apr 02 12:19:09 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Thu Apr 02 12:49:53 2020 +0200
@@ -9,7 +9,7 @@
   val is_active: unit -> bool
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
-  exception EXIT of exn
+  exception EXIT of int
   val crashes: exn list Synchronized.var
   val init_options: unit -> unit
   val init_options_interactive: unit -> unit
@@ -98,7 +98,7 @@
 
 (* init protocol -- uninterruptible *)
 
-exception EXIT of exn;
+exception EXIT of int;
 
 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
@@ -186,7 +186,7 @@
             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
+          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;
 
@@ -205,8 +205,11 @@
     val _ = Message_Channel.shutdown msg_channel;
     val _ = BinIO.closeIn in_stream;
     val _ = BinIO.closeOut out_stream;
-
-  in Exn.release result end);
+  in
+    (case result of
+      Exn.Exn (EXIT rc) => exit rc
+    | _ => Exn.release result)
+  end);
 
 end;
 
diff -r dad29591645a -r 3e121f999120 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Apr 02 12:19:09 2020 +0200
+++ b/src/Pure/Tools/build.ML	Thu Apr 02 12:49:53 2020 +0200
@@ -258,9 +258,9 @@
               (build_session args; []) handle exn =>
               (Runtime.exn_message_list exn handle _ (*sic!*) =>
                 (build_session_finished ["CRASHED"];
-                  raise Isabelle_Process.EXIT exn))) ();
+                  raise Isabelle_Process.EXIT 1))) ();
           val _ = build_session_finished errs;
-        in if null errs then () else raise Isabelle_Process.EXIT (Command_Line.EXIT 1) end
+        in if null errs then () else raise Isabelle_Process.EXIT 1 end
       | _ => raise Match);
 
 end;