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