src/Pure/System/isabelle_process.ML

 *)
 
 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
   val init: unit -> unit
   val init_build: unit -> unit

 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
 
 
 (* protocol commands *)
 
+exception STOP;
+exception EXIT of int;
+
+val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false;
+
 local
 
 val commands =
   Synchronized.var "Isabelle_Process.commands"
     (Symtab.empty: (string list -> unit) Symtab.table);

 fun run_command name args =
   (case Symtab.lookup (Synchronized.value commands) name of
     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;
 
 
 (* restricted tracing messages *)

       end);
 
 
 (* init protocol -- uninterruptible *)
 
-exception EXIT of int;
-
 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
 local
 
 fun recover crash =

 
     (* protocol *)
 
     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 ();
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());

     val _ = Future.shutdown ();
     val _ = Execution.reset ();
     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);
 
 end;