--- 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;