src/Pure/PIDE/exec.ML
author wenzelm
Thu, 11 Jul 2013 18:41:05 +0200
changeset 52602 00170ef1dc39
parent 52596 40298d383463
child 52604 ff2f0818aebc
permissions -rw-r--r--
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/PIDE/exec.ML
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
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     4
Global management of command execution fragments.
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     5
*)
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     6
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     7
signature EXEC =
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     8
sig
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
     9
  val running: Document_ID.exec -> unit
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    10
  val finished: Document_ID.exec -> bool -> unit
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    11
  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
    12
  val peek_running: Document_ID.exec -> Future.group option
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    13
  val purge_unstable: unit -> unit
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    14
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    15
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    16
structure Exec: EXEC =
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    17
struct
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    18
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    19
type status = Future.group option;  (*SOME group: running, NONE: canceled/unstable*)
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    20
val execs = Synchronized.var "Exec.execs" (Inttab.empty: status Inttab.table);
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    21
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    22
fun running exec_id =
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    23
  let
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    24
    val group =
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    25
      (case Future.worker_group () of
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    26
        SOME group => group
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    27
      | NONE => error ("Missing worker thread context for execution " ^ Document_ID.print exec_id));
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    28
  in Synchronized.change execs (Inttab.update_new (exec_id, SOME group)) end;
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    29
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    30
fun finished exec_id stable =
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    31
  Synchronized.change execs
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    32
    (if stable then Inttab.delete exec_id else Inttab.update (exec_id, NONE));
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    33
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    34
fun is_stable exec_id =
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    35
  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    36
  (case Inttab.lookup (Synchronized.value execs) exec_id of
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    37
    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
    38
  | SOME status => is_some status);
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    39
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    40
fun peek_running exec_id =
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    41
  (case Inttab.lookup (Synchronized.value execs) exec_id of
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    42
    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
    43
  | _ => NONE);
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    44
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    45
fun purge_unstable () =
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    46
  Synchronized.guarded_access execs
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    47
    (fn tab =>
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    48
      let
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    49
        val unstable = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) tab [];
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    50
        val tab' = fold Inttab.delete unstable tab;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    51
      in SOME ((), tab') end);
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    52
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    53
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    54