src/Pure/PIDE/execution.ML
changeset 52605 a2a805549c74
parent 52604 ff2f0818aebc
child 52606 0d68d108d7e0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 11:07:02 2013 +0200
     1.3 @@ -0,0 +1,100 @@
     1.4 +(*  Title:      Pure/PIDE/execution.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Global management of command execution fragments.
     1.8 +*)
     1.9 +
    1.10 +signature EXECUTION =
    1.11 +sig
    1.12 +  type context
    1.13 +  val no_context: context
    1.14 +  val drop_context: context -> unit
    1.15 +  val fresh_context: unit -> context
    1.16 +  val is_running: context -> bool
    1.17 +  val running: context -> Document_ID.exec -> bool
    1.18 +  val finished: Document_ID.exec -> bool -> unit
    1.19 +  val is_stable: Document_ID.exec -> bool
    1.20 +  val peek_running: Document_ID.exec -> Future.group option
    1.21 +  val purge_canceled: unit -> unit
    1.22 +  val terminate_all: unit -> unit
    1.23 +end;
    1.24 +
    1.25 +structure Execution: EXECUTION =
    1.26 +struct
    1.27 +
    1.28 +(* global state *)
    1.29 +
    1.30 +datatype context = Context of Document_ID.generic;
    1.31 +val no_context = Context Document_ID.none;
    1.32 +
    1.33 +type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    1.34 +val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
    1.35 +
    1.36 +
    1.37 +(* unique execution context *)
    1.38 +
    1.39 +fun drop_context context =
    1.40 +  Synchronized.change state
    1.41 +    (apfst (fn context' => if context = context' then no_context else context'));
    1.42 +
    1.43 +fun fresh_context () =
    1.44 +  let
    1.45 +    val context = Context (Document_ID.make ());
    1.46 +    val _ = Synchronized.change state (apfst (K context));
    1.47 +  in context end;
    1.48 +
    1.49 +fun is_running context = context = fst (Synchronized.value state);
    1.50 +
    1.51 +
    1.52 +(* registered execs *)
    1.53 +
    1.54 +fun running context exec_id =
    1.55 +  Synchronized.guarded_access state
    1.56 +    (fn (current_context, execs) =>
    1.57 +      let
    1.58 +        val cont = context = current_context;
    1.59 +        val execs' =
    1.60 +          if cont then
    1.61 +            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
    1.62 +              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    1.63 +          else execs;
    1.64 +      in SOME (cont, (current_context, execs')) end);
    1.65 +
    1.66 +fun finished exec_id stable =
    1.67 +  Synchronized.change state
    1.68 +    (apsnd (fn execs =>
    1.69 +      if not (Inttab.defined execs exec_id) then
    1.70 +        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
    1.71 +      else if stable then Inttab.delete exec_id execs
    1.72 +      else Inttab.update (exec_id, NONE) execs));
    1.73 +
    1.74 +fun is_stable exec_id =
    1.75 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    1.76 +  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    1.77 +    NONE => true
    1.78 +  | SOME status => is_some status);
    1.79 +
    1.80 +fun peek_running exec_id =
    1.81 +  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    1.82 +    SOME (SOME group) => SOME group
    1.83 +  | _ => NONE);
    1.84 +
    1.85 +fun purge_canceled () =
    1.86 +  Synchronized.guarded_access state
    1.87 +    (fn (context, execs) =>
    1.88 +      let
    1.89 +        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
    1.90 +        val execs' = fold Inttab.delete canceled execs;
    1.91 +      in SOME ((), (context, execs')) end);
    1.92 +
    1.93 +fun terminate_all () =
    1.94 +  let
    1.95 +    val groups =
    1.96 +      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
    1.97 +        (snd (Synchronized.value state)) [];
    1.98 +    val _ = List.app Future.cancel_group groups;
    1.99 +    val _ = List.app Future.terminate groups;
   1.100 +  in () end;
   1.101 +
   1.102 +end;
   1.103 +