# HG changeset patch
# User wenzelm
# Date 1375178834 -7200
# Node ID c143ad7811fc00c18773ac92c8605d7c1e61bda1
# Parent  9795ea6549053951b0498346ff2c39682f99540e
pro-forma Execution.reset, despite lack of final join/commit;

diff -r 9795ea654905 -r c143ad7811fc src/Pure/PIDE/execution.ML
--- 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 ();
diff -r 9795ea654905 -r c143ad7811fc src/Pure/System/isabelle_process.ML
--- 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;