src/Pure/PIDE/execution.ML
author wenzelm
Tue Jul 30 11:38:43 2013 +0200 (2013-07-30 ago)
changeset 52784 4ba2e8b9972f
parent 52775 e0169f13bd37
child 52787 c143ad7811fc
permissions -rw-r--r--
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
     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 fragments.
     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 is_running_exec: Document_ID.exec -> bool
    14   val running: Document_ID.execution -> Document_ID.exec -> bool
    15   val cancel: Document_ID.exec -> unit
    16   val terminate: Document_ID.exec -> unit
    17 end;
    18 
    19 structure Execution: EXECUTION =
    20 struct
    21 
    22 val state =
    23   Synchronized.var "Execution.state"
    24     (Document_ID.none, Inttab.empty: Future.group Inttab.table);
    25 
    26 
    27 (* unique running execution *)
    28 
    29 fun start () =
    30   let
    31     val execution_id = Document_ID.make ();
    32     val _ = Synchronized.change state (apfst (K execution_id));
    33   in execution_id end;
    34 
    35 fun discontinue () =
    36   Synchronized.change state (apfst (K Document_ID.none));
    37 
    38 fun is_running execution_id = execution_id = fst (Synchronized.value state);
    39 
    40 
    41 (* registered execs *)
    42 
    43 fun is_running_exec exec_id =
    44   Inttab.defined (snd (Synchronized.value state)) exec_id;
    45 
    46 fun running execution_id exec_id =
    47   Synchronized.guarded_access state
    48     (fn (execution_id', execs) =>
    49       let
    50         val continue = execution_id = execution_id';
    51         val execs' =
    52           if continue then
    53             Inttab.update_new (exec_id, Future.the_worker_group ()) execs
    54               handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    55           else execs;
    56       in SOME (continue, (execution_id', execs')) end);
    57 
    58 fun peek_list exec_id =
    59   the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
    60 
    61 fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
    62 fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
    63 
    64 end;
    65