src/Pure/PIDE/execution.ML
author wenzelm
Fri Jul 12 11:28:03 2013 +0200 (2013-07-12 ago)
changeset 52606 0d68d108d7e0
parent 52605 a2a805549c74
child 52607 33a133d50616
permissions -rw-r--r--
tuned signature;
tuned comments;
     1 (*  Title:      Pure/PIDE/execution.ML
     2     Author:     Makarius
     3 
     4 Global management of execution.  Unique running execution serves as
     5 barrier for further exploration of exec particles.
     6 *)
     7 
     8 signature EXECUTION =
     9 sig
    10   val start: unit -> Document_ID.execution
    11   val discontinue: unit -> unit
    12   val is_running: Document_ID.execution -> bool
    13   val running: Document_ID.execution -> Document_ID.exec -> bool
    14   val finished: Document_ID.exec -> bool -> unit
    15   val is_stable: Document_ID.exec -> bool
    16   val peek_running: Document_ID.exec -> Future.group option
    17   val purge_canceled: unit -> unit
    18   val terminate_all: unit -> unit
    19 end;
    20 
    21 structure Execution: EXECUTION =
    22 struct
    23 
    24 type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    25 val state = Synchronized.var "Execution.state" (Document_ID.none, Inttab.empty: status Inttab.table);
    26 
    27 
    28 (* unique running execution *)
    29 
    30 fun start () =
    31   let
    32     val execution_id = Document_ID.make ();
    33     val _ = Synchronized.change state (apfst (K execution_id));
    34   in execution_id end;
    35 
    36 fun discontinue () =
    37   Synchronized.change state (apfst (K Document_ID.none));
    38 
    39 fun is_running execution_id = execution_id = fst (Synchronized.value state);
    40 
    41 
    42 (* registered execs *)
    43 
    44 fun running execution_id exec_id =
    45   Synchronized.guarded_access state
    46     (fn (execution_id', execs) =>
    47       let
    48         val continue = execution_id = execution_id';
    49         val execs' =
    50           if continue then
    51             Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
    52               handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    53           else execs;
    54       in SOME (continue, (execution_id', execs')) end);
    55 
    56 fun finished exec_id stable =
    57   Synchronized.change state
    58     (apsnd (fn execs =>
    59       if not (Inttab.defined execs exec_id) then
    60         error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
    61       else if stable then Inttab.delete exec_id execs
    62       else Inttab.update (exec_id, NONE) execs));
    63 
    64 fun is_stable exec_id =
    65   not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    66   (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    67     NONE => true
    68   | SOME status => is_some status);
    69 
    70 fun peek_running exec_id =
    71   (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    72     SOME (SOME group) => SOME group
    73   | _ => NONE);
    74 
    75 fun purge_canceled () =
    76   Synchronized.guarded_access state
    77     (fn (execution_id, execs) =>
    78       let
    79         val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
    80         val execs' = fold Inttab.delete canceled execs;
    81       in SOME ((), (execution_id, execs')) end);
    82 
    83 fun terminate_all () =
    84   let
    85     val groups =
    86       Inttab.fold (fn (_, SOME group) => cons group | _ => I)
    87         (snd (Synchronized.value state)) [];
    88     val _ = List.app Future.cancel_group groups;
    89     val _ = List.app Future.terminate groups;
    90   in () end;
    91 
    92 end;
    93