src/Pure/PIDE/execution.ML

clarified module name;

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