src/Pure/PIDE/execution.ML

 barrier for further exploration of exec fragments.
 *)
 
 signature EXECUTION =
 sig
+  val reset: unit -> unit
   val start: unit -> Document_ID.execution
   val discontinue: unit -> unit
   val is_running: Document_ID.execution -> bool
   val is_running_exec: Document_ID.exec -> bool
   val running: Document_ID.execution -> Document_ID.exec -> bool

 end;
 
 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 ();
     val _ = Synchronized.change state (apfst (K execution_id));