src/Pure/PIDE/execution.ML
author wenzelm
Fri Jul 12 11:07:02 2013 +0200 (2013-07-12 ago)
changeset 52605 a2a805549c74
parent 52604 src/Pure/PIDE/exec.ML@ff2f0818aebc
child 52606 0d68d108d7e0
permissions -rw-r--r--
clarified module name;
wenzelm@52605
     1
(*  Title:      Pure/PIDE/execution.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@52605
     7
signature EXECUTION =
wenzelm@52596
     8
sig
wenzelm@52604
     9
  type context
wenzelm@52604
    10
  val no_context: context
wenzelm@52604
    11
  val drop_context: context -> unit
wenzelm@52604
    12
  val fresh_context: unit -> context
wenzelm@52604
    13
  val is_running: context -> bool
wenzelm@52604
    14
  val running: context -> Document_ID.exec -> bool
wenzelm@52602
    15
  val finished: Document_ID.exec -> bool -> unit
wenzelm@52596
    16
  val is_stable: Document_ID.exec -> bool
wenzelm@52602
    17
  val peek_running: Document_ID.exec -> Future.group option
wenzelm@52604
    18
  val purge_canceled: unit -> unit
wenzelm@52604
    19
  val terminate_all: unit -> unit
wenzelm@52596
    20
end;
wenzelm@52596
    21
wenzelm@52605
    22
structure Execution: EXECUTION =
wenzelm@52596
    23
struct
wenzelm@52596
    24
wenzelm@52604
    25
(* global state *)
wenzelm@52604
    26
wenzelm@52604
    27
datatype context = Context of Document_ID.generic;
wenzelm@52604
    28
val no_context = Context Document_ID.none;
wenzelm@52604
    29
wenzelm@52604
    30
type status = Future.group option;  (*SOME group: running, NONE: canceled*)
wenzelm@52605
    31
val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
wenzelm@52602
    32
wenzelm@52604
    33
wenzelm@52604
    34
(* unique execution context *)
wenzelm@52604
    35
wenzelm@52604
    36
fun drop_context context =
wenzelm@52604
    37
  Synchronized.change state
wenzelm@52604
    38
    (apfst (fn context' => if context = context' then no_context else context'));
wenzelm@52604
    39
wenzelm@52604
    40
fun fresh_context () =
wenzelm@52602
    41
  let
wenzelm@52604
    42
    val context = Context (Document_ID.make ());
wenzelm@52604
    43
    val _ = Synchronized.change state (apfst (K context));
wenzelm@52604
    44
  in context end;
wenzelm@52604
    45
wenzelm@52604
    46
fun is_running context = context = fst (Synchronized.value state);
wenzelm@52604
    47
wenzelm@52604
    48
wenzelm@52604
    49
(* registered execs *)
wenzelm@52604
    50
wenzelm@52604
    51
fun running context exec_id =
wenzelm@52604
    52
  Synchronized.guarded_access state
wenzelm@52604
    53
    (fn (current_context, execs) =>
wenzelm@52604
    54
      let
wenzelm@52604
    55
        val cont = context = current_context;
wenzelm@52604
    56
        val execs' =
wenzelm@52604
    57
          if cont then
wenzelm@52604
    58
            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
wenzelm@52604
    59
              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
wenzelm@52604
    60
          else execs;
wenzelm@52604
    61
      in SOME (cont, (current_context, execs')) end);
wenzelm@52602
    62
wenzelm@52602
    63
fun finished exec_id stable =
wenzelm@52604
    64
  Synchronized.change state
wenzelm@52604
    65
    (apsnd (fn execs =>
wenzelm@52604
    66
      if not (Inttab.defined execs exec_id) then
wenzelm@52604
    67
        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
wenzelm@52604
    68
      else if stable then Inttab.delete exec_id execs
wenzelm@52604
    69
      else Inttab.update (exec_id, NONE) execs));
wenzelm@52596
    70
wenzelm@52596
    71
fun is_stable exec_id =
wenzelm@52596
    72
  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
wenzelm@52604
    73
  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
wenzelm@52596
    74
    NONE => true
wenzelm@52602
    75
  | SOME status => is_some status);
wenzelm@52596
    76
wenzelm@52602
    77
fun peek_running exec_id =
wenzelm@52604
    78
  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
wenzelm@52602
    79
    SOME (SOME group) => SOME group
wenzelm@52602
    80
  | _ => NONE);
wenzelm@52596
    81
wenzelm@52604
    82
fun purge_canceled () =
wenzelm@52604
    83
  Synchronized.guarded_access state
wenzelm@52604
    84
    (fn (context, execs) =>
wenzelm@52596
    85
      let
wenzelm@52604
    86
        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
wenzelm@52604
    87
        val execs' = fold Inttab.delete canceled execs;
wenzelm@52604
    88
      in SOME ((), (context, execs')) end);
wenzelm@52604
    89
wenzelm@52604
    90
fun terminate_all () =
wenzelm@52604
    91
  let
wenzelm@52604
    92
    val groups =
wenzelm@52604
    93
      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
wenzelm@52604
    94
        (snd (Synchronized.value state)) [];
wenzelm@52604
    95
    val _ = List.app Future.cancel_group groups;
wenzelm@52604
    96
    val _ = List.app Future.terminate groups;
wenzelm@52604
    97
  in () end;
wenzelm@52596
    98
wenzelm@52596
    99
end;
wenzelm@52596
   100