src/Pure/PIDE/execution.ML
changeset 52605 a2a805549c74
parent 52604 ff2f0818aebc
child 52606 0d68d108d7e0
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 11:07:02 2013 +0200
@@ -0,0 +1,100 @@
+(*  Title:      Pure/PIDE/execution.ML
+    Author:     Makarius
+
+Global management of command execution fragments.
+*)
+
+signature EXECUTION =
+sig
+  type context
+  val no_context: context
+  val drop_context: context -> unit
+  val fresh_context: unit -> context
+  val is_running: context -> bool
+  val running: context -> Document_ID.exec -> bool
+  val finished: Document_ID.exec -> bool -> unit
+  val is_stable: Document_ID.exec -> bool
+  val peek_running: Document_ID.exec -> Future.group option
+  val purge_canceled: unit -> unit
+  val terminate_all: unit -> unit
+end;
+
+structure Execution: EXECUTION =
+struct
+
+(* global state *)
+
+datatype context = Context of Document_ID.generic;
+val no_context = Context Document_ID.none;
+
+type status = Future.group option;  (*SOME group: running, NONE: canceled*)
+val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
+
+
+(* unique execution context *)
+
+fun drop_context context =
+  Synchronized.change state
+    (apfst (fn context' => if context = context' then no_context else context'));
+
+fun fresh_context () =
+  let
+    val context = Context (Document_ID.make ());
+    val _ = Synchronized.change state (apfst (K context));
+  in context end;
+
+fun is_running context = context = fst (Synchronized.value state);
+
+
+(* registered execs *)
+
+fun running context exec_id =
+  Synchronized.guarded_access state
+    (fn (current_context, execs) =>
+      let
+        val cont = context = current_context;
+        val execs' =
+          if cont then
+            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
+              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
+          else execs;
+      in SOME (cont, (current_context, execs')) end);
+
+fun finished exec_id stable =
+  Synchronized.change state
+    (apsnd (fn execs =>
+      if not (Inttab.defined execs exec_id) then
+        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
+      else if stable then Inttab.delete exec_id execs
+      else Inttab.update (exec_id, NONE) execs));
+
+fun is_stable exec_id =
+  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
+  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
+    NONE => true
+  | SOME status => is_some status);
+
+fun peek_running exec_id =
+  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
+    SOME (SOME group) => SOME group
+  | _ => NONE);
+
+fun purge_canceled () =
+  Synchronized.guarded_access state
+    (fn (context, execs) =>
+      let
+        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
+        val execs' = fold Inttab.delete canceled execs;
+      in SOME ((), (context, execs')) end);
+
+fun terminate_all () =
+  let
+    val groups =
+      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
+        (snd (Synchronized.value state)) [];
+    val _ = List.app Future.cancel_group groups;
+    val _ = List.app Future.terminate groups;
+  in () end;
+
+end;
+