src/Pure/PIDE/execution.ML
author wenzelm
Tue, 30 Jul 2013 11:38:43 +0200
changeset 52784 4ba2e8b9972f
parent 52775 e0169f13bd37
child 52787 c143ad7811fc
permissions -rw-r--r--
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
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
52608
wenzelm
parents: 52607
diff changeset
     5
barrier for further exploration of exec fragments.
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
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    13
  val is_running_exec: Document_ID.exec -> bool
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    14
  val running: Document_ID.execution -> Document_ID.exec -> bool
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    15
  val cancel: Document_ID.exec -> unit
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    16
  val terminate: Document_ID.exec -> unit
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    17
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    18
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
    19
structure Execution: EXECUTION =
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    20
struct
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    21
52607
33a133d50616 clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents: 52606
diff changeset
    22
val state =
33a133d50616 clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents: 52606
diff changeset
    23
  Synchronized.var "Execution.state"
33a133d50616 clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents: 52606
diff changeset
    24
    (Document_ID.none, Inttab.empty: Future.group 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
    25
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    26
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    27
(* unique running execution *)
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    28
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    29
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
    30
  let
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    31
    val execution_id = Document_ID.make ();
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    32
    val _ = Synchronized.change state (apfst (K execution_id));
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    33
  in execution_id end;
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    34
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    35
fun discontinue () =
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    36
  Synchronized.change state (apfst (K Document_ID.none));
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    37
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    38
fun is_running execution_id = execution_id = fst (Synchronized.value state);
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    39
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    40
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    41
(* registered execs *)
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    42
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    43
fun is_running_exec exec_id =
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    44
  Inttab.defined (snd (Synchronized.value state)) exec_id;
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    45
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    46
fun running execution_id exec_id =
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    47
  Synchronized.guarded_access state
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    48
    (fn (execution_id', execs) =>
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    49
      let
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    50
        val continue = execution_id = execution_id';
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    51
        val execs' =
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    52
          if continue then
52607
33a133d50616 clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents: 52606
diff changeset
    53
            Inttab.update_new (exec_id, Future.the_worker_group ()) execs
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    54
              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    55
          else execs;
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    56
      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
    57
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    58
fun peek_list exec_id =
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    59
  the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    60
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    61
fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    62
fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    63
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    64
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    65