--- a/src/Pure/PIDE/execution.ML Mon Jul 29 22:17:32 2013 +0200
+++ b/src/Pure/PIDE/execution.ML Tue Jul 30 11:38:43 2013 +0200
@@ -10,6 +10,7 @@
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
val cancel: Document_ID.exec -> unit
val terminate: Document_ID.exec -> unit
@@ -39,6 +40,9 @@
(* registered execs *)
+fun is_running_exec exec_id =
+ Inttab.defined (snd (Synchronized.value state)) exec_id;
+
fun running execution_id exec_id =
Synchronized.guarded_access state
(fn (execution_id', execs) =>