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