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;
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@52607
    14
  val finished: Document_ID.exec -> unit
wenzelm@52655
    15
  val cancel: Document_ID.exec -> unit
wenzelm@52655
    16
  val terminate: Document_ID.exec -> unit
wenzelm@52607
    17
  val snapshot: unit -> Future.group list
wenzelm@52596
    18
end;
wenzelm@52596
    19
wenzelm@52605
    20
structure Execution: EXECUTION =
wenzelm@52596
    21
struct
wenzelm@52596
    22
wenzelm@52607
    23
val state =
wenzelm@52607
    24
  Synchronized.var "Execution.state"
wenzelm@52607
    25
    (Document_ID.none, Inttab.empty: Future.group Inttab.table);
wenzelm@52602
    26
wenzelm@52604
    27
wenzelm@52606
    28
(* unique running execution *)
wenzelm@52604
    29
wenzelm@52606
    30
fun start () =
wenzelm@52602
    31
  let
wenzelm@52606
    32
    val execution_id = Document_ID.make ();
wenzelm@52606
    33
    val _ = Synchronized.change state (apfst (K execution_id));
wenzelm@52606
    34
  in execution_id end;
wenzelm@52604
    35
wenzelm@52606
    36
fun discontinue () =
wenzelm@52606
    37
  Synchronized.change state (apfst (K Document_ID.none));
wenzelm@52606
    38
wenzelm@52606
    39
fun is_running execution_id = execution_id = fst (Synchronized.value state);
wenzelm@52604
    40
wenzelm@52604
    41
wenzelm@52604
    42
(* registered execs *)
wenzelm@52604
    43
wenzelm@52606
    44
fun running execution_id exec_id =
wenzelm@52604
    45
  Synchronized.guarded_access state
wenzelm@52606
    46
    (fn (execution_id', execs) =>
wenzelm@52604
    47
      let
wenzelm@52606
    48
        val continue = execution_id = execution_id';
wenzelm@52604
    49
        val execs' =
wenzelm@52606
    50
          if continue then
wenzelm@52607
    51
            Inttab.update_new (exec_id, Future.the_worker_group ()) execs
wenzelm@52604
    52
              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
wenzelm@52604
    53
          else execs;
wenzelm@52606
    54
      in SOME (continue, (execution_id', execs')) end);
wenzelm@52602
    55
wenzelm@52607
    56
fun finished exec_id =
wenzelm@52604
    57
  Synchronized.change state
wenzelm@52604
    58
    (apsnd (fn execs =>
wenzelm@52608
    59
      Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
wenzelm@52608
    60
        error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
wenzelm@52596
    61
wenzelm@52655
    62
fun peek_list exec_id =
wenzelm@52655
    63
  the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
wenzelm@52655
    64
wenzelm@52655
    65
fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
wenzelm@52655
    66
fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
wenzelm@52604
    67
wenzelm@52607
    68
fun snapshot () =
wenzelm@52607
    69
  Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
wenzelm@52596
    70
wenzelm@52596
    71
end;
wenzelm@52596
    72