src/Pure/PIDE/execution.ML
author wenzelm
Fri Jul 12 12:17:03 2013 +0200 (2013-07-12 ago)
changeset 52608 f03c6a4d5870
parent 52607 33a133d50616
child 52655 3b2b1ef13979
permissions -rw-r--r--
tuned;
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@52607
    15
  val peek: Document_ID.exec -> Future.group option
wenzelm@52607
    16
  val snapshot: unit -> Future.group list
wenzelm@52596
    17
end;
wenzelm@52596
    18
wenzelm@52605
    19
structure Execution: EXECUTION =
wenzelm@52596
    20
struct
wenzelm@52596
    21
wenzelm@52607
    22
val state =
wenzelm@52607
    23
  Synchronized.var "Execution.state"
wenzelm@52607
    24
    (Document_ID.none, Inttab.empty: Future.group Inttab.table);
wenzelm@52602
    25
wenzelm@52604
    26
wenzelm@52606
    27
(* unique running execution *)
wenzelm@52604
    28
wenzelm@52606
    29
fun start () =
wenzelm@52602
    30
  let
wenzelm@52606
    31
    val execution_id = Document_ID.make ();
wenzelm@52606
    32
    val _ = Synchronized.change state (apfst (K execution_id));
wenzelm@52606
    33
  in execution_id end;
wenzelm@52604
    34
wenzelm@52606
    35
fun discontinue () =
wenzelm@52606
    36
  Synchronized.change state (apfst (K Document_ID.none));
wenzelm@52606
    37
wenzelm@52606
    38
fun is_running execution_id = execution_id = fst (Synchronized.value state);
wenzelm@52604
    39
wenzelm@52604
    40
wenzelm@52604
    41
(* registered execs *)
wenzelm@52604
    42
wenzelm@52606
    43
fun running execution_id exec_id =
wenzelm@52604
    44
  Synchronized.guarded_access state
wenzelm@52606
    45
    (fn (execution_id', execs) =>
wenzelm@52604
    46
      let
wenzelm@52606
    47
        val continue = execution_id = execution_id';
wenzelm@52604
    48
        val execs' =
wenzelm@52606
    49
          if continue then
wenzelm@52607
    50
            Inttab.update_new (exec_id, Future.the_worker_group ()) execs
wenzelm@52604
    51
              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
wenzelm@52604
    52
          else execs;
wenzelm@52606
    53
      in SOME (continue, (execution_id', execs')) end);
wenzelm@52602
    54
wenzelm@52607
    55
fun finished exec_id =
wenzelm@52604
    56
  Synchronized.change state
wenzelm@52604
    57
    (apsnd (fn execs =>
wenzelm@52608
    58
      Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
wenzelm@52608
    59
        error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
wenzelm@52596
    60
wenzelm@52607
    61
fun peek exec_id =
wenzelm@52607
    62
  Inttab.lookup (snd (Synchronized.value state)) exec_id;
wenzelm@52604
    63
wenzelm@52607
    64
fun snapshot () =
wenzelm@52607
    65
  Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
wenzelm@52596
    66
wenzelm@52596
    67
end;
wenzelm@52596
    68