author | wenzelm |
Tue, 08 Aug 2017 12:21:29 +0200 | |
changeset 66378 | 53a6c5d4d03e |
parent 66371 | 6ce1afc01040 |
child 67659 | 11b390e971f6 |
permissions | -rw-r--r-- |
52605 | 1 |
(* Title: Pure/PIDE/execution.ML |
52596 | 2 |
Author: Makarius |
3 |
||
52606 | 4 |
Global management of execution. Unique running execution serves as |
53192 | 5 |
barrier for further exploration of forked command execs. |
52596 | 6 |
*) |
7 |
||
52605 | 8 |
signature EXECUTION = |
52596 | 9 |
sig |
52606 | 10 |
val start: unit -> Document_ID.execution |
11 |
val discontinue: unit -> unit |
|
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 |
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53193
diff
changeset
|
14 |
val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool |
66370 | 15 |
val snapshot: Document_ID.exec list -> Future.task list |
66371
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
16 |
val join: Document_ID.exec list -> unit |
53192 | 17 |
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
|
18 |
val cancel: Document_ID.exec -> unit |
56292 | 19 |
type params = {name: string, pos: Position.T, pri: int} |
20 |
val fork: params -> (unit -> 'a) -> 'a future |
|
56305 | 21 |
val print: params -> (unit -> unit) -> unit |
56292 | 22 |
val fork_prints: Document_ID.exec -> unit |
53192 | 23 |
val purge: Document_ID.exec list -> unit |
24 |
val reset: unit -> Future.group list |
|
25 |
val shutdown: unit -> unit |
|
52596 | 26 |
end; |
27 |
||
52605 | 28 |
structure Execution: EXECUTION = |
52596 | 29 |
struct |
30 |
||
52787
c143ad7811fc
pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents:
52784
diff
changeset
|
31 |
(* global state *) |
c143ad7811fc
pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents:
52784
diff
changeset
|
32 |
|
56292 | 33 |
type print = {name: string, pri: int, body: unit -> unit}; |
34 |
type exec_state = Future.group list * print list; (*active forks, prints*) |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
35 |
type state = |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
36 |
Document_ID.execution * (*overall document execution*) |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
37 |
exec_state Inttab.table; (*running command execs*) |
52787
c143ad7811fc
pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents:
52784
diff
changeset
|
38 |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
39 |
val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]); |
52787
c143ad7811fc
pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents:
52784
diff
changeset
|
40 |
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
|
41 |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
42 |
fun get_state () = Synchronized.value state; |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
43 |
fun change_state_result f = Synchronized.change_result state f; |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
44 |
fun change_state f = Synchronized.change state f; |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
45 |
|
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
46 |
fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id; |
53192 | 47 |
|
52604 | 48 |
|
52606 | 49 |
(* unique running execution *) |
52604 | 50 |
|
52606 | 51 |
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
|
52 |
let |
52606 | 53 |
val execution_id = Document_ID.make (); |
53192 | 54 |
val _ = change_state (apfst (K execution_id)); |
52606 | 55 |
in execution_id end; |
52604 | 56 |
|
53192 | 57 |
fun discontinue () = change_state (apfst (K Document_ID.none)); |
52606 | 58 |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
59 |
fun is_running execution_id = execution_id = #1 (get_state ()); |
52604 | 60 |
|
61 |
||
66371
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
62 |
(* running execs *) |
52604 | 63 |
|
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52775
diff
changeset
|
64 |
fun is_running_exec exec_id = |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
65 |
Inttab.defined (#2 (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
|
66 |
|
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53193
diff
changeset
|
67 |
fun running execution_id exec_id groups = |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
68 |
change_state_result (fn (execution_id', execs) => |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
69 |
let |
59348
8a6788917b32
do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
wenzelm
parents:
56333
diff
changeset
|
70 |
val ok = execution_id = execution_id' andalso not (Inttab.defined execs exec_id); |
8a6788917b32
do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
wenzelm
parents:
56333
diff
changeset
|
71 |
val execs' = execs |> ok ? Inttab.update (exec_id, (groups, [])); |
8a6788917b32
do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
wenzelm
parents:
56333
diff
changeset
|
72 |
in (ok, (execution_id', execs')) end); |
53192 | 73 |
|
66371
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
74 |
|
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
75 |
(* exec groups and tasks *) |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
76 |
|
66370 | 77 |
fun exec_groups ((_, execs): state) exec_id = |
78 |
(case Inttab.lookup execs exec_id of |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
79 |
SOME (groups, _) => groups |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
80 |
| NONE => []); |
53192 | 81 |
|
66370 | 82 |
fun snapshot exec_ids = |
66378 | 83 |
change_state_result (`(fn state => Future.snapshot (maps (exec_groups state) exec_ids))); |
66370 | 84 |
|
66371
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
85 |
fun join exec_ids = |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
86 |
(case snapshot exec_ids of |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
87 |
[] => () |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
88 |
| tasks => |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
89 |
((singleton o Future.forks) |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
90 |
{name = "Execution.join", group = SOME (Future.new_group NONE), |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
91 |
deps = tasks, pri = 0, interrupts = false} I |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
92 |
|> Future.join; join exec_ids)); |
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset
|
93 |
|
66370 | 94 |
fun peek exec_id = exec_groups (get_state ()) exec_id; |
95 |
||
53192 | 96 |
fun cancel exec_id = List.app Future.cancel_group (peek exec_id); |
97 |
||
98 |
||
99 |
(* fork *) |
|
100 |
||
101 |
fun status task markups = |
|
56296
5413b6379c0e
less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents:
56292
diff
changeset
|
102 |
let |
5413b6379c0e
less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents:
56292
diff
changeset
|
103 |
val props = |
5413b6379c0e
less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents:
56292
diff
changeset
|
104 |
if ! Multithreading.trace >= 2 |
5413b6379c0e
less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents:
56292
diff
changeset
|
105 |
then [(Markup.taskN, Task_Queue.str_of_task task)] else []; |
5413b6379c0e
less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents:
56292
diff
changeset
|
106 |
in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end; |
53192 | 107 |
|
56292 | 108 |
type params = {name: string, pos: Position.T, pri: int}; |
109 |
||
110 |
fun fork ({name, pos, pri}: params) e = |
|
62923 | 111 |
Thread_Attributes.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () => |
53192 | 112 |
let |
113 |
val exec_id = the_default 0 (Position.parse_id pos); |
|
114 |
val group = Future.worker_subgroup (); |
|
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53193
diff
changeset
|
115 |
val _ = change_state (apsnd (fn execs => |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
116 |
(case Inttab.lookup execs exec_id of |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
117 |
SOME (groups, prints) => |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
118 |
Inttab.update (exec_id, (group :: groups, prints)) execs |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
119 |
| NONE => raise Fail (unregistered exec_id)))); |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52608
diff
changeset
|
120 |
|
53192 | 121 |
val future = |
122 |
(singleton o Future.forks) |
|
123 |
{name = name, group = SOME group, deps = [], pri = pri, interrupts = false} |
|
124 |
(fn () => |
|
125 |
let |
|
126 |
val task = the (Future.worker_task ()); |
|
127 |
val _ = status task [Markup.running]; |
|
128 |
val result = |
|
129 |
Exn.capture (Future.interruptible_task e) () |
|
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
59467
diff
changeset
|
130 |
|> Future.identify_result pos |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
59467
diff
changeset
|
131 |
|> Exn.map_exn Runtime.thread_context; |
54646
2b38549374ba
more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents:
53375
diff
changeset
|
132 |
val _ = status task [Markup.joined]; |
53192 | 133 |
val _ = |
134 |
(case result of |
|
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54646
diff
changeset
|
135 |
Exn.Exn exn => |
54646
2b38549374ba
more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents:
53375
diff
changeset
|
136 |
(status task [Markup.failed]; |
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54646
diff
changeset
|
137 |
status task [Markup.finished]; |
64677
8dc24130e8fe
more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents:
62923
diff
changeset
|
138 |
Output.report [Markup.markup_only (Markup.bad ())]; |
54646
2b38549374ba
more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents:
53375
diff
changeset
|
139 |
if exec_id = 0 then () |
65948 | 140 |
else List.app (Future.error_message pos) (Runtime.exn_messages exn)) |
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54646
diff
changeset
|
141 |
| Exn.Res _ => |
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54646
diff
changeset
|
142 |
status task [Markup.finished]) |
53192 | 143 |
in Exn.release result end); |
54646
2b38549374ba
more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents:
53375
diff
changeset
|
144 |
|
53192 | 145 |
val _ = status (Future.task_of future) [Markup.forked]; |
146 |
in future end)) (); |
|
52604 | 147 |
|
53192 | 148 |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
149 |
(* print *) |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
150 |
|
56305 | 151 |
fun print ({name, pos, pri}: params) e = |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
152 |
change_state (apsnd (fn execs => |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
153 |
let |
56292 | 154 |
val exec_id = the_default 0 (Position.parse_id pos); |
56305 | 155 |
val print = {name = name, pri = pri, body = e}; |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
156 |
in |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
157 |
(case Inttab.lookup execs exec_id of |
56292 | 158 |
SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
159 |
| NONE => raise Fail (unregistered exec_id)) |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
160 |
end)); |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
161 |
|
56292 | 162 |
fun fork_prints exec_id = |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
163 |
(case Inttab.lookup (#2 (get_state ())) exec_id of |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
164 |
SOME (_, prints) => |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
165 |
if null prints orelse null (tl prints) orelse not (Multithreading.enabled ()) |
56292 | 166 |
then List.app (fn {body, ...} => body ()) (rev prints) |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
167 |
else |
56296
5413b6379c0e
less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents:
56292
diff
changeset
|
168 |
let val pos = Position.thread_data () in |
56292 | 169 |
List.app (fn {name, pri, body} => |
170 |
ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints) |
|
171 |
end |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
172 |
| NONE => raise Fail (unregistered exec_id)); |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
173 |
|
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
174 |
|
53192 | 175 |
(* cleanup *) |
176 |
||
177 |
fun purge exec_ids = |
|
178 |
(change_state o apsnd) (fn execs => |
|
179 |
let |
|
180 |
val execs' = fold Inttab.delete_safe exec_ids execs; |
|
181 |
val () = |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
182 |
(execs', ()) |-> Inttab.fold (fn (exec_id, (groups, _)) => fn () => |
53192 | 183 |
if Inttab.defined execs' exec_id then () |
184 |
else groups |> List.app (fn group => |
|
185 |
if Task_Queue.is_canceled group then () |
|
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53193
diff
changeset
|
186 |
else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id))); |
53192 | 187 |
in execs' end); |
188 |
||
189 |
fun reset () = |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
190 |
change_state_result (fn (_, execs) => |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
54678
diff
changeset
|
191 |
let val groups = Inttab.fold (append o #1 o #2) execs [] |
53192 | 192 |
in (groups, init_state) end); |
193 |
||
194 |
fun shutdown () = |
|
195 |
(Future.shutdown (); |
|
196 |
(case maps Task_Queue.group_status (reset ()) of |
|
197 |
[] => () |
|
198 |
| exns => raise Par_Exn.make exns)); |
|
199 |
||
200 |
end; |
|
201 |