src/Pure/PIDE/execution.ML
author wenzelm
Sun, 25 Aug 2013 20:32:26 +0200
changeset 53192 04df1d236e1c
parent 52787 c143ad7811fc
child 53193 2ddc5e788f7c
permissions -rw-r--r--
maintain goal forks as part of global execution; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
     1
(*  Title:      Pure/PIDE/execution.ML
52596
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
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
     4
Global management of execution.  Unique running execution serves as
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
     5
barrier for further exploration of forked command execs.
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     6
*)
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     7
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
     8
signature EXECUTION =
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     9
sig
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    10
  val start: unit -> Document_ID.execution
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    11
  val discontinue: unit -> unit
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    12
  val is_running: Document_ID.execution -> bool
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    13
  val is_running_exec: Document_ID.exec -> bool
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    14
  val running: Document_ID.execution -> Document_ID.exec -> bool
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    15
  val peek: Document_ID.exec -> Future.group list
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    16
  val cancel: Document_ID.exec -> unit
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    17
  val terminate: Document_ID.exec -> unit
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    18
  val fork: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    19
  val purge: Document_ID.exec list -> unit
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    20
  val reset: unit -> Future.group list
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    21
  val shutdown: unit -> unit
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    22
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    23
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
    24
structure Execution: EXECUTION =
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    25
struct
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    26
52787
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    27
(* global state *)
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    28
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    29
datatype state = State of
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    30
  {execution: Document_ID.execution,  (*overall document execution*)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    31
   execs: Future.group list Inttab.table};  (*command execs with registered forks*)
52787
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    32
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    33
fun make_state (execution, execs) = State {execution = execution, execs = execs};
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    34
fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    35
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    36
val init_state = make_state (Document_ID.none, Inttab.empty);
52787
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    37
val state = Synchronized.var "Execution.state" init_state;
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    38
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    39
fun get_state () = let val State args = Synchronized.value state in args end;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    40
fun change_state f = Synchronized.change state (map_state f);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    41
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    42
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    43
(* unique running execution *)
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    44
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    45
fun start () =
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    46
  let
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    47
    val execution_id = Document_ID.make ();
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    48
    val _ = change_state (apfst (K execution_id));
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    49
  in execution_id end;
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    50
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    51
fun discontinue () = change_state (apfst (K Document_ID.none));
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    52
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    53
fun is_running execution_id = execution_id = #execution (get_state ());
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    54
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    55
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    56
(* execs *)
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    57
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    58
fun is_running_exec exec_id =
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    59
  Inttab.defined (#execs (get_state ())) exec_id;
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    60
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    61
fun running execution_id exec_id =
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    62
  Synchronized.guarded_access state
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    63
    (fn State {execution = execution_id', execs} =>
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    64
      let
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    65
        val continue = execution_id = execution_id';
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    66
        val execs' =
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    67
          if continue then
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    68
            Inttab.update_new (exec_id, [Future.the_worker_group ()]) execs
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    69
              handle Inttab.DUP dup =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    70
                error ("Execution already registered: " ^ Document_ID.print dup)
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    71
          else execs;
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    72
      in SOME (continue, make_state (execution_id', execs')) end);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    73
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    74
fun peek exec_id =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    75
  Inttab.lookup_list (#execs (get_state ())) exec_id;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    76
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    77
fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    78
fun terminate exec_id = List.app Future.terminate (peek exec_id);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    79
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    80
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    81
(* fork *)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    82
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    83
local
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    84
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    85
fun status task markups =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    86
  let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    87
  in Output.status (implode (map (Markup.markup_only o props) markups)) end;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    88
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    89
fun register exec =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    90
  change_state (fn (execution, execs) => (execution, Inttab.cons_list exec execs));
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    91
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    92
in
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    93
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    94
fun fork {name, pos, pri} e =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    95
  uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    96
    let
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    97
      val exec_id = the_default 0 (Position.parse_id pos);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    98
      val group = Future.worker_subgroup ();
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    99
      val _ = register (exec_id, group);
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
   100
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   101
      val future =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   102
        (singleton o Future.forks)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   103
          {name = name, group = SOME group, deps = [], pri = pri, interrupts = false}
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   104
          (fn () =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   105
            let
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   106
              val task = the (Future.worker_task ());
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   107
              val _ = status task [Markup.running];
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   108
              val result =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   109
                Exn.capture (Future.interruptible_task e) ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   110
                |> Future.identify_result pos;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   111
              val _ = status task [Markup.finished, Markup.joined];
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   112
              val _ =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   113
                (case result of
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   114
                  Exn.Res _ => ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   115
                | Exn.Exn exn =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   116
                    if exec_id = 0 orelse Exn.is_interrupt exn then ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   117
                    else
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   118
                      (status task [Markup.failed];
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   119
                       Output.report (Markup.markup_only Markup.bad);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   120
                       List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   121
            in Exn.release result end);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   122
      val _ = status (Future.task_of future) [Markup.forked];
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   123
    in future end)) ();
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
   124
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
   125
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
   126
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   127
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   128
(* cleanup *)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   129
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   130
fun purge exec_ids =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   131
  (change_state o apsnd) (fn execs =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   132
    let
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   133
      val execs' = fold Inttab.delete_safe exec_ids execs;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   134
      val () =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   135
        (execs', ()) |-> Inttab.fold (fn (exec_id, groups) => fn () =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   136
          if Inttab.defined execs' exec_id then ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   137
          else groups |> List.app (fn group =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   138
            if Task_Queue.is_canceled group then ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   139
            else error ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   140
    in execs' end);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   141
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   142
fun reset () =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   143
  Synchronized.change_result state (fn State {execs, ...} =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   144
    let val groups = Inttab.fold (append o #2) execs []
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   145
    in (groups, init_state) end);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   146
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   147
fun shutdown () =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   148
  (Future.shutdown ();
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   149
    (case maps Task_Queue.group_status (reset ()) of
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   150
      [] => ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   151
    | exns => raise Par_Exn.make exns));
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   152
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   153
end;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   154