src/Pure/PIDE/exec.ML
author wenzelm
Thu Jul 11 18:41:05 2013 +0200 (2013-07-11 ago)
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;
wenzelm@52596
     1
(*  Title:      Pure/PIDE/exec.ML
wenzelm@52596
     2
    Author:     Makarius
wenzelm@52596
     3
wenzelm@52596
     4
Global management of command execution fragments.
wenzelm@52596
     5
*)
wenzelm@52596
     6
wenzelm@52596
     7
signature EXEC =
wenzelm@52596
     8
sig
wenzelm@52602
     9
  val running: Document_ID.exec -> unit
wenzelm@52602
    10
  val finished: Document_ID.exec -> bool -> unit
wenzelm@52596
    11
  val is_stable: Document_ID.exec -> bool
wenzelm@52602
    12
  val peek_running: Document_ID.exec -> Future.group option
wenzelm@52596
    13
  val purge_unstable: unit -> unit
wenzelm@52596
    14
end;
wenzelm@52596
    15
wenzelm@52596
    16
structure Exec: EXEC =
wenzelm@52596
    17
struct
wenzelm@52596
    18
wenzelm@52602
    19
type status = Future.group option;  (*SOME group: running, NONE: canceled/unstable*)
wenzelm@52602
    20
val execs = Synchronized.var "Exec.execs" (Inttab.empty: status Inttab.table);
wenzelm@52602
    21
wenzelm@52602
    22
fun running exec_id =
wenzelm@52602
    23
  let
wenzelm@52602
    24
    val group =
wenzelm@52602
    25
      (case Future.worker_group () of
wenzelm@52602
    26
        SOME group => group
wenzelm@52602
    27
      | NONE => error ("Missing worker thread context for execution " ^ Document_ID.print exec_id));
wenzelm@52602
    28
  in Synchronized.change execs (Inttab.update_new (exec_id, SOME group)) end;
wenzelm@52602
    29
wenzelm@52602
    30
fun finished exec_id stable =
wenzelm@52602
    31
  Synchronized.change execs
wenzelm@52602
    32
    (if stable then Inttab.delete exec_id else Inttab.update (exec_id, NONE));
wenzelm@52596
    33
wenzelm@52596
    34
fun is_stable exec_id =
wenzelm@52596
    35
  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
wenzelm@52602
    36
  (case Inttab.lookup (Synchronized.value execs) exec_id of
wenzelm@52596
    37
    NONE => true
wenzelm@52602
    38
  | SOME status => is_some status);
wenzelm@52596
    39
wenzelm@52602
    40
fun peek_running exec_id =
wenzelm@52602
    41
  (case Inttab.lookup (Synchronized.value execs) exec_id of
wenzelm@52602
    42
    SOME (SOME group) => SOME group
wenzelm@52602
    43
  | _ => NONE);
wenzelm@52596
    44
wenzelm@52596
    45
fun purge_unstable () =
wenzelm@52602
    46
  Synchronized.guarded_access execs
wenzelm@52596
    47
    (fn tab =>
wenzelm@52596
    48
      let
wenzelm@52602
    49
        val unstable = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) tab [];
wenzelm@52596
    50
        val tab' = fold Inttab.delete unstable tab;
wenzelm@52596
    51
      in SOME ((), tab') end);
wenzelm@52596
    52
wenzelm@52596
    53
end;
wenzelm@52596
    54