--- a/src/Pure/PIDE/execution.ML Tue Jul 30 11:54:57 2013 +0200
+++ b/src/Pure/PIDE/execution.ML Tue Jul 30 12:07:14 2013 +0200
@@ -7,6 +7,7 @@
signature EXECUTION =
sig
+ val reset: unit -> unit
val start: unit -> Document_ID.execution
val discontinue: unit -> unit
val is_running: Document_ID.execution -> bool
@@ -19,13 +20,18 @@
structure Execution: EXECUTION =
struct
-val state =
- Synchronized.var "Execution.state"
- (Document_ID.none, Inttab.empty: Future.group Inttab.table);
+(* global state *)
+
+type state = Document_ID.execution * Future.group Inttab.table;
+
+val init_state: state = (Document_ID.none, Inttab.empty);
+val state = Synchronized.var "Execution.state" init_state;
(* unique running execution *)
+fun reset () = Synchronized.change state (K init_state);
+
fun start () =
let
val execution_id = Document_ID.make ();
--- a/src/Pure/System/isabelle_process.ML Tue Jul 30 11:54:57 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Jul 30 12:07:14 2013 +0200
@@ -182,7 +182,7 @@
| exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
in
if continue then loop channel
- else (Future.shutdown (); Goal.reset_futures (); ())
+ else (Future.shutdown (); Goal.reset_futures (); Execution.reset ())
end;
end;