src/Pure/PIDE/execution.ML
author wenzelm
Fri, 12 Jul 2013 11:28:03 +0200
changeset 52606 0d68d108d7e0
parent 52605 a2a805549c74
child 52607 33a133d50616
permissions -rw-r--r--
tuned signature; tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
     1
(*  Title:      Pure/PIDE/execution.ML
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     3
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
     4
Global management of execution.  Unique running execution serves as
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
     5
barrier for further exploration of exec particles.
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     6
*)
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     7
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
     8
signature EXECUTION =
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     9
sig
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    10
  val start: unit -> Document_ID.execution
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    11
  val discontinue: unit -> unit
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    12
  val is_running: Document_ID.execution -> bool
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    13
  val running: Document_ID.execution -> Document_ID.exec -> bool
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    14
  val finished: Document_ID.exec -> bool -> unit
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    15
  val is_stable: Document_ID.exec -> bool
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    16
  val peek_running: Document_ID.exec -> Future.group option
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    17
  val purge_canceled: unit -> unit
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    18
  val terminate_all: unit -> unit
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    19
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    20
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
    21
structure Execution: EXECUTION =
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    22
struct
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    23
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    24
type status = Future.group option;  (*SOME group: running, NONE: canceled*)
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    25
val state = Synchronized.var "Execution.state" (Document_ID.none, Inttab.empty: status Inttab.table);
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    26
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    27
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    28
(* unique running execution *)
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    29
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    30
fun start () =
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    31
  let
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    32
    val execution_id = Document_ID.make ();
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    33
    val _ = Synchronized.change state (apfst (K execution_id));
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    34
  in execution_id end;
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    35
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    36
fun discontinue () =
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    37
  Synchronized.change state (apfst (K Document_ID.none));
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    38
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    39
fun is_running execution_id = execution_id = fst (Synchronized.value state);
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    40
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    41
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    42
(* registered execs *)
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    43
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    44
fun running execution_id exec_id =
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    45
  Synchronized.guarded_access state
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    46
    (fn (execution_id', execs) =>
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    47
      let
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    48
        val continue = execution_id = execution_id';
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    49
        val execs' =
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    50
          if continue then
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    51
            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    52
              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    53
          else execs;
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    54
      in SOME (continue, (execution_id', execs')) end);
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    55
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    56
fun finished exec_id stable =
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    57
  Synchronized.change state
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    58
    (apsnd (fn execs =>
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    59
      if not (Inttab.defined execs exec_id) then
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    60
        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    61
      else if stable then Inttab.delete exec_id execs
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    62
      else Inttab.update (exec_id, NONE) execs));
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    63
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    64
fun is_stable exec_id =
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    65
  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    66
  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    67
    NONE => true
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    68
  | SOME status => is_some status);
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    69
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    70
fun peek_running exec_id =
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    71
  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    72
    SOME (SOME group) => SOME group
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    73
  | _ => NONE);
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    74
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    75
fun purge_canceled () =
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    76
  Synchronized.guarded_access state
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    77
    (fn (execution_id, execs) =>
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    78
      let
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    79
        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    80
        val execs' = fold Inttab.delete canceled execs;
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    81
      in SOME ((), (execution_id, execs')) end);
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    82
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    83
fun terminate_all () =
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    84
  let
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    85
    val groups =
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    86
      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    87
        (snd (Synchronized.value state)) [];
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    88
    val _ = List.app Future.cancel_group groups;
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    89
    val _ = List.app Future.terminate groups;
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    90
  in () end;
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    91
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    92
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    93