src/Pure/PIDE/exec.ML
author wenzelm
Thu Jul 11 14:42:11 2013 +0200 (2013-07-11 ago)
changeset 52596 40298d383463
child 52602 00170ef1dc39
permissions -rw-r--r--
global management of command execution fragments;
tuned;
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@52596
     9
  val is_stable: Document_ID.exec -> bool
wenzelm@52596
    10
  val running: Document_ID.exec -> unit
wenzelm@52596
    11
  val finished: Document_ID.exec -> unit
wenzelm@52596
    12
  val canceled: Document_ID.exec -> unit
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@52596
    19
val running_execs =
wenzelm@52596
    20
  Synchronized.var "Exec.running_execs" (Inttab.empty: {stable: bool} Inttab.table);
wenzelm@52596
    21
wenzelm@52596
    22
fun is_stable exec_id =
wenzelm@52596
    23
  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
wenzelm@52596
    24
  (case Inttab.lookup (Synchronized.value running_execs) exec_id of
wenzelm@52596
    25
    NONE => true
wenzelm@52596
    26
  | SOME {stable} => stable);
wenzelm@52596
    27
wenzelm@52596
    28
fun running exec_id =
wenzelm@52596
    29
  Synchronized.change running_execs (Inttab.update_new (exec_id, {stable = true}));
wenzelm@52596
    30
wenzelm@52596
    31
fun finished exec_id =
wenzelm@52596
    32
  Synchronized.change running_execs (Inttab.delete exec_id);
wenzelm@52596
    33
wenzelm@52596
    34
fun canceled exec_id =
wenzelm@52596
    35
  Synchronized.change running_execs (Inttab.update (exec_id, {stable = false}));
wenzelm@52596
    36
wenzelm@52596
    37
fun purge_unstable () =
wenzelm@52596
    38
  Synchronized.guarded_access running_execs
wenzelm@52596
    39
    (fn tab =>
wenzelm@52596
    40
      let
wenzelm@52596
    41
        val unstable = Inttab.fold (fn (exec_id, {stable = false}) => cons exec_id | _ => I) tab [];
wenzelm@52596
    42
        val tab' = fold Inttab.delete unstable tab;
wenzelm@52596
    43
      in SOME ((), tab') end);
wenzelm@52596
    44
wenzelm@52596
    45
end;
wenzelm@52596
    46