src/Pure/PIDE/exec.ML

--- a/src/Pure/PIDE/exec.ML	Thu Jul 11 16:35:37 2013 +0200
+++ b/src/Pure/PIDE/exec.ML	Thu Jul 11 18:41:05 2013 +0200
@@ -6,39 +6,47 @@
 
 signature EXEC =
 sig
+  val running: Document_ID.exec -> unit
+  val finished: Document_ID.exec -> bool -> unit
   val is_stable: Document_ID.exec -> bool
-  val running: Document_ID.exec -> unit
-  val finished: Document_ID.exec -> unit
-  val canceled: Document_ID.exec -> unit
+  val peek_running: Document_ID.exec -> Future.group option
   val purge_unstable: unit -> unit
 end;
 
 structure Exec: EXEC =
 struct
 
-val running_execs =
-  Synchronized.var "Exec.running_execs" (Inttab.empty: {stable: bool} Inttab.table);
+type status = Future.group option;  (*SOME group: running, NONE: canceled/unstable*)
+val execs = Synchronized.var "Exec.execs" (Inttab.empty: status Inttab.table);
+
+fun running exec_id =
+  let
+    val group =
+      (case Future.worker_group () of
+        SOME group => group
+      | NONE => error ("Missing worker thread context for execution " ^ Document_ID.print exec_id));
+  in Synchronized.change execs (Inttab.update_new (exec_id, SOME group)) end;
+
+fun finished exec_id stable =
+  Synchronized.change execs
+    (if stable then Inttab.delete exec_id else Inttab.update (exec_id, NONE));
 
 fun is_stable exec_id =
   not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
-  (case Inttab.lookup (Synchronized.value running_execs) exec_id of
+  (case Inttab.lookup (Synchronized.value execs) exec_id of
     NONE => true
-  | SOME {stable} => stable);
+  | SOME status => is_some status);
 
-fun running exec_id =
-  Synchronized.change running_execs (Inttab.update_new (exec_id, {stable = true}));
-
-fun finished exec_id =
-  Synchronized.change running_execs (Inttab.delete exec_id);
-
-fun canceled exec_id =
-  Synchronized.change running_execs (Inttab.update (exec_id, {stable = false}));
+fun peek_running exec_id =
+  (case Inttab.lookup (Synchronized.value execs) exec_id of
+    SOME (SOME group) => SOME group
+  | _ => NONE);
 
 fun purge_unstable () =
-  Synchronized.guarded_access running_execs
+  Synchronized.guarded_access execs
     (fn tab =>
       let
-        val unstable = Inttab.fold (fn (exec_id, {stable = false}) => cons exec_id | _ => I) tab [];
+        val unstable = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) tab [];
         val tab' = fold Inttab.delete unstable tab;
       in SOME ((), tab') end);