(* 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;