src/Pure/PIDE/execution.ML
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52608 f03c6a4d5870
child 52760 8517172b9626
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
     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 running: Document_ID.execution -> Document_ID.exec -> bool
    14   val finished: Document_ID.exec -> unit
    15   val cancel: Document_ID.exec -> unit
    16   val terminate: Document_ID.exec -> unit
    17   val snapshot: unit -> Future.group list
    18 end;
    19 
    20 structure Execution: EXECUTION =
    21 struct
    22 
    23 val state =
    24   Synchronized.var "Execution.state"
    25     (Document_ID.none, Inttab.empty: Future.group 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, 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 =
    57   Synchronized.change state
    58     (apsnd (fn execs =>
    59       Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
    60         error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
    61 
    62 fun peek_list exec_id =
    63   the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
    64 
    65 fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
    66 fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
    67 
    68 fun snapshot () =
    69   Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
    70 
    71 end;
    72