src/Pure/PIDE/execution.ML
author wenzelm
Thu Dec 05 20:22:53 2013 +0100 (2013-12-05 ago)
changeset 54678 87910da843d5
parent 54646 2b38549374ba
child 56291 e79f76a48449
permissions -rw-r--r--
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
tuned signature;
wenzelm@52605
     1
(*  Title:      Pure/PIDE/execution.ML
wenzelm@52596
     2
    Author:     Makarius
wenzelm@52596
     3
wenzelm@52606
     4
Global management of execution.  Unique running execution serves as
wenzelm@53192
     5
barrier for further exploration of forked command execs.
wenzelm@52596
     6
*)
wenzelm@52596
     7
wenzelm@52605
     8
signature EXECUTION =
wenzelm@52596
     9
sig
wenzelm@52606
    10
  val start: unit -> Document_ID.execution
wenzelm@52606
    11
  val discontinue: unit -> unit
wenzelm@52606
    12
  val is_running: Document_ID.execution -> bool
wenzelm@52784
    13
  val is_running_exec: Document_ID.exec -> bool
wenzelm@53375
    14
  val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
wenzelm@53192
    15
  val peek: Document_ID.exec -> Future.group list
wenzelm@52655
    16
  val cancel: Document_ID.exec -> unit
wenzelm@52655
    17
  val terminate: Document_ID.exec -> unit
wenzelm@53192
    18
  val fork: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
wenzelm@53192
    19
  val purge: Document_ID.exec list -> unit
wenzelm@53192
    20
  val reset: unit -> Future.group list
wenzelm@53192
    21
  val shutdown: unit -> unit
wenzelm@52596
    22
end;
wenzelm@52596
    23
wenzelm@52605
    24
structure Execution: EXECUTION =
wenzelm@52596
    25
struct
wenzelm@52596
    26
wenzelm@52787
    27
(* global state *)
wenzelm@52787
    28
wenzelm@53192
    29
datatype state = State of
wenzelm@53192
    30
  {execution: Document_ID.execution,  (*overall document execution*)
wenzelm@53192
    31
   execs: Future.group list Inttab.table};  (*command execs with registered forks*)
wenzelm@52787
    32
wenzelm@53192
    33
fun make_state (execution, execs) = State {execution = execution, execs = execs};
wenzelm@53192
    34
fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
wenzelm@53192
    35
wenzelm@53375
    36
val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
wenzelm@52787
    37
val state = Synchronized.var "Execution.state" init_state;
wenzelm@52602
    38
wenzelm@53192
    39
fun get_state () = let val State args = Synchronized.value state in args end;
wenzelm@53192
    40
fun change_state f = Synchronized.change state (map_state f);
wenzelm@53192
    41
wenzelm@52604
    42
wenzelm@52606
    43
(* unique running execution *)
wenzelm@52604
    44
wenzelm@52606
    45
fun start () =
wenzelm@52602
    46
  let
wenzelm@52606
    47
    val execution_id = Document_ID.make ();
wenzelm@53192
    48
    val _ = change_state (apfst (K execution_id));
wenzelm@52606
    49
  in execution_id end;
wenzelm@52604
    50
wenzelm@53192
    51
fun discontinue () = change_state (apfst (K Document_ID.none));
wenzelm@52606
    52
wenzelm@53192
    53
fun is_running execution_id = execution_id = #execution (get_state ());
wenzelm@52604
    54
wenzelm@52604
    55
wenzelm@53192
    56
(* execs *)
wenzelm@52604
    57
wenzelm@52784
    58
fun is_running_exec exec_id =
wenzelm@53192
    59
  Inttab.defined (#execs (get_state ())) exec_id;
wenzelm@52784
    60
wenzelm@53375
    61
fun running execution_id exec_id groups =
wenzelm@53375
    62
  Synchronized.change_result state
wenzelm@53192
    63
    (fn State {execution = execution_id', execs} =>
wenzelm@52604
    64
      let
wenzelm@52606
    65
        val continue = execution_id = execution_id';
wenzelm@52604
    66
        val execs' =
wenzelm@52606
    67
          if continue then
wenzelm@53375
    68
            Inttab.update_new (exec_id, groups) execs
wenzelm@53192
    69
              handle Inttab.DUP dup =>
wenzelm@53375
    70
                raise Fail ("Execution already registered: " ^ Document_ID.print dup)
wenzelm@52604
    71
          else execs;
wenzelm@53375
    72
      in (continue, make_state (execution_id', execs')) end);
wenzelm@53192
    73
wenzelm@53192
    74
fun peek exec_id =
wenzelm@53192
    75
  Inttab.lookup_list (#execs (get_state ())) exec_id;
wenzelm@53192
    76
wenzelm@53192
    77
fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
wenzelm@53192
    78
fun terminate exec_id = List.app Future.terminate (peek exec_id);
wenzelm@53192
    79
wenzelm@53192
    80
wenzelm@53192
    81
(* fork *)
wenzelm@53192
    82
wenzelm@53192
    83
fun status task markups =
wenzelm@53192
    84
  let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
wenzelm@53192
    85
  in Output.status (implode (map (Markup.markup_only o props) markups)) end;
wenzelm@53192
    86
wenzelm@53192
    87
fun fork {name, pos, pri} e =
wenzelm@53192
    88
  uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
wenzelm@53192
    89
    let
wenzelm@53192
    90
      val exec_id = the_default 0 (Position.parse_id pos);
wenzelm@53192
    91
      val group = Future.worker_subgroup ();
wenzelm@53375
    92
      val _ = change_state (apsnd (fn execs =>
wenzelm@53375
    93
        if Inttab.defined execs exec_id
wenzelm@53375
    94
        then Inttab.cons_list (exec_id, group) execs
wenzelm@53375
    95
        else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
wenzelm@52655
    96
wenzelm@53192
    97
      val future =
wenzelm@53192
    98
        (singleton o Future.forks)
wenzelm@53192
    99
          {name = name, group = SOME group, deps = [], pri = pri, interrupts = false}
wenzelm@53192
   100
          (fn () =>
wenzelm@53192
   101
            let
wenzelm@53192
   102
              val task = the (Future.worker_task ());
wenzelm@53192
   103
              val _ = status task [Markup.running];
wenzelm@53192
   104
              val result =
wenzelm@53192
   105
                Exn.capture (Future.interruptible_task e) ()
wenzelm@53192
   106
                |> Future.identify_result pos;
wenzelm@54646
   107
              val _ = status task [Markup.joined];
wenzelm@53192
   108
              val _ =
wenzelm@53192
   109
                (case result of
wenzelm@54678
   110
                  Exn.Exn exn =>
wenzelm@54646
   111
                   (status task [Markup.failed];
wenzelm@54678
   112
                    status task [Markup.finished];
wenzelm@54646
   113
                    Output.report (Markup.markup_only Markup.bad);
wenzelm@54646
   114
                    if exec_id = 0 then ()
wenzelm@54678
   115
                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
wenzelm@54678
   116
                | Exn.Res _ =>
wenzelm@54678
   117
                    status task [Markup.finished])
wenzelm@53192
   118
            in Exn.release result end);
wenzelm@54646
   119
wenzelm@53192
   120
      val _ = status (Future.task_of future) [Markup.forked];
wenzelm@53192
   121
    in future end)) ();
wenzelm@52604
   122
wenzelm@53192
   123
wenzelm@53192
   124
(* cleanup *)
wenzelm@53192
   125
wenzelm@53192
   126
fun purge exec_ids =
wenzelm@53192
   127
  (change_state o apsnd) (fn execs =>
wenzelm@53192
   128
    let
wenzelm@53192
   129
      val execs' = fold Inttab.delete_safe exec_ids execs;
wenzelm@53192
   130
      val () =
wenzelm@53192
   131
        (execs', ()) |-> Inttab.fold (fn (exec_id, groups) => fn () =>
wenzelm@53192
   132
          if Inttab.defined execs' exec_id then ()
wenzelm@53192
   133
          else groups |> List.app (fn group =>
wenzelm@53192
   134
            if Task_Queue.is_canceled group then ()
wenzelm@53375
   135
            else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
wenzelm@53192
   136
    in execs' end);
wenzelm@53192
   137
wenzelm@53192
   138
fun reset () =
wenzelm@53192
   139
  Synchronized.change_result state (fn State {execs, ...} =>
wenzelm@53192
   140
    let val groups = Inttab.fold (append o #2) execs []
wenzelm@53192
   141
    in (groups, init_state) end);
wenzelm@53192
   142
wenzelm@53192
   143
fun shutdown () =
wenzelm@53192
   144
  (Future.shutdown ();
wenzelm@53192
   145
    (case maps Task_Queue.group_status (reset ()) of
wenzelm@53192
   146
      [] => ()
wenzelm@53192
   147
    | exns => raise Par_Exn.make exns));
wenzelm@53192
   148
wenzelm@53192
   149
end;
wenzelm@53192
   150