src/Pure/PIDE/execution.ML
author wenzelm
Mon Jul 29 18:59:58 2013 +0200 (2013-07-29 ago)
changeset 52775 e0169f13bd37
parent 52760 8517172b9626
child 52784 4ba2e8b9972f
permissions -rw-r--r--
keep memo_exec execution running, which is important to cancel goal forks eventually;
run as nested worker task to keep main group valid, even after cancelation of removed subgroups;
do not memoize interrupt, but absorb it silently in main execution;
Goal.purge_futures: rough sanity check of group status;
wenzelm@52605
     1
(*  Title:      Pure/PIDE/execution.ML
wenzelm@52596
     2
    Author:     Makarius
wenzelm@52596
     3
wenzelm@52606
     4
Global management of execution.  Unique running execution serves as
wenzelm@52608
     5
barrier for further exploration of exec fragments.
wenzelm@52596
     6
*)
wenzelm@52596
     7
wenzelm@52605
     8
signature EXECUTION =
wenzelm@52596
     9
sig
wenzelm@52606
    10
  val start: unit -> Document_ID.execution
wenzelm@52606
    11
  val discontinue: unit -> unit
wenzelm@52606
    12
  val is_running: Document_ID.execution -> bool
wenzelm@52606
    13
  val running: Document_ID.execution -> Document_ID.exec -> bool
wenzelm@52655
    14
  val cancel: Document_ID.exec -> unit
wenzelm@52655
    15
  val terminate: Document_ID.exec -> unit
wenzelm@52596
    16
end;
wenzelm@52596
    17
wenzelm@52605
    18
structure Execution: EXECUTION =
wenzelm@52596
    19
struct
wenzelm@52596
    20
wenzelm@52607
    21
val state =
wenzelm@52607
    22
  Synchronized.var "Execution.state"
wenzelm@52607
    23
    (Document_ID.none, Inttab.empty: Future.group Inttab.table);
wenzelm@52602
    24
wenzelm@52604
    25
wenzelm@52606
    26
(* unique running execution *)
wenzelm@52604
    27
wenzelm@52606
    28
fun start () =
wenzelm@52602
    29
  let
wenzelm@52606
    30
    val execution_id = Document_ID.make ();
wenzelm@52606
    31
    val _ = Synchronized.change state (apfst (K execution_id));
wenzelm@52606
    32
  in execution_id end;
wenzelm@52604
    33
wenzelm@52606
    34
fun discontinue () =
wenzelm@52606
    35
  Synchronized.change state (apfst (K Document_ID.none));
wenzelm@52606
    36
wenzelm@52606
    37
fun is_running execution_id = execution_id = fst (Synchronized.value state);
wenzelm@52604
    38
wenzelm@52604
    39
wenzelm@52604
    40
(* registered execs *)
wenzelm@52604
    41
wenzelm@52606
    42
fun running execution_id exec_id =
wenzelm@52604
    43
  Synchronized.guarded_access state
wenzelm@52606
    44
    (fn (execution_id', execs) =>
wenzelm@52604
    45
      let
wenzelm@52606
    46
        val continue = execution_id = execution_id';
wenzelm@52604
    47
        val execs' =
wenzelm@52606
    48
          if continue then
wenzelm@52607
    49
            Inttab.update_new (exec_id, Future.the_worker_group ()) execs
wenzelm@52604
    50
              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
wenzelm@52604
    51
          else execs;
wenzelm@52606
    52
      in SOME (continue, (execution_id', execs')) end);
wenzelm@52602
    53
wenzelm@52655
    54
fun peek_list exec_id =
wenzelm@52655
    55
  the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
wenzelm@52655
    56
wenzelm@52655
    57
fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
wenzelm@52655
    58
fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
wenzelm@52604
    59
wenzelm@52596
    60
end;
wenzelm@52596
    61