diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Mar 30 19:39:11 2020 +0200
@@ -9,6 +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
   val crashes: exn list Synchronized.var
   val init_options: unit -> unit
   val init_options_interactive: unit -> unit
@@ -143,6 +144,8 @@
 
 (* protocol loop -- uninterruptible *)
 
+exception EXIT of exn;
+
 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
 local
@@ -152,6 +155,8 @@
     Output.physical_stderr
       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
 
+fun shutdown () = (Future.shutdown (); ignore (Execution.reset ()));
+
 in
 
 fun loop stream =
@@ -161,11 +166,9 @@
         NONE => false
       | SOME [] => (Output.system_message "Isabelle process: no input"; true)
       | SOME (name :: args) => (run_command name args; true))
-      handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
-  in
-    if continue then loop stream
-    else (Future.shutdown (); Execution.reset (); ())
-  end;
+      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;
 
 end;