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