1 (* Title: Pure/PIDE/execution.ML |
1 (* Title: Pure/PIDE/execution.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Global management of command execution fragments. |
4 Global management of execution. Unique running execution serves as |
|
5 barrier for further exploration of exec particles. |
5 *) |
6 *) |
6 |
7 |
7 signature EXECUTION = |
8 signature EXECUTION = |
8 sig |
9 sig |
9 type context |
10 val start: unit -> Document_ID.execution |
10 val no_context: context |
11 val discontinue: unit -> unit |
11 val drop_context: context -> unit |
12 val is_running: Document_ID.execution -> bool |
12 val fresh_context: unit -> context |
13 val running: Document_ID.execution -> Document_ID.exec -> bool |
13 val is_running: context -> bool |
|
14 val running: context -> Document_ID.exec -> bool |
|
15 val finished: Document_ID.exec -> bool -> unit |
14 val finished: Document_ID.exec -> bool -> unit |
16 val is_stable: Document_ID.exec -> bool |
15 val is_stable: Document_ID.exec -> bool |
17 val peek_running: Document_ID.exec -> Future.group option |
16 val peek_running: Document_ID.exec -> Future.group option |
18 val purge_canceled: unit -> unit |
17 val purge_canceled: unit -> unit |
19 val terminate_all: unit -> unit |
18 val terminate_all: unit -> unit |
20 end; |
19 end; |
21 |
20 |
22 structure Execution: EXECUTION = |
21 structure Execution: EXECUTION = |
23 struct |
22 struct |
24 |
23 |
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*) |
24 type status = Future.group option; (*SOME group: running, NONE: canceled*) |
31 val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table); |
25 val state = Synchronized.var "Execution.state" (Document_ID.none, Inttab.empty: status Inttab.table); |
32 |
26 |
33 |
27 |
34 (* unique execution context *) |
28 (* unique running execution *) |
35 |
29 |
36 fun drop_context context = |
30 fun start () = |
37 Synchronized.change state |
31 let |
38 (apfst (fn context' => if context = context' then no_context else context')); |
32 val execution_id = Document_ID.make (); |
|
33 val _ = Synchronized.change state (apfst (K execution_id)); |
|
34 in execution_id end; |
39 |
35 |
40 fun fresh_context () = |
36 fun discontinue () = |
41 let |
37 Synchronized.change state (apfst (K Document_ID.none)); |
42 val context = Context (Document_ID.make ()); |
|
43 val _ = Synchronized.change state (apfst (K context)); |
|
44 in context end; |
|
45 |
38 |
46 fun is_running context = context = fst (Synchronized.value state); |
39 fun is_running execution_id = execution_id = fst (Synchronized.value state); |
47 |
40 |
48 |
41 |
49 (* registered execs *) |
42 (* registered execs *) |
50 |
43 |
51 fun running context exec_id = |
44 fun running execution_id exec_id = |
52 Synchronized.guarded_access state |
45 Synchronized.guarded_access state |
53 (fn (current_context, execs) => |
46 (fn (execution_id', execs) => |
54 let |
47 let |
55 val cont = context = current_context; |
48 val continue = execution_id = execution_id'; |
56 val execs' = |
49 val execs' = |
57 if cont then |
50 if continue then |
58 Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs |
51 Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs |
59 handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup) |
52 handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup) |
60 else execs; |
53 else execs; |
61 in SOME (cont, (current_context, execs')) end); |
54 in SOME (continue, (execution_id', execs')) end); |
62 |
55 |
63 fun finished exec_id stable = |
56 fun finished exec_id stable = |
64 Synchronized.change state |
57 Synchronized.change state |
65 (apsnd (fn execs => |
58 (apsnd (fn execs => |
66 if not (Inttab.defined execs exec_id) then |
59 if not (Inttab.defined execs exec_id) then |
79 SOME (SOME group) => SOME group |
72 SOME (SOME group) => SOME group |
80 | _ => NONE); |
73 | _ => NONE); |
81 |
74 |
82 fun purge_canceled () = |
75 fun purge_canceled () = |
83 Synchronized.guarded_access state |
76 Synchronized.guarded_access state |
84 (fn (context, execs) => |
77 (fn (execution_id, execs) => |
85 let |
78 let |
86 val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs []; |
79 val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs []; |
87 val execs' = fold Inttab.delete canceled execs; |
80 val execs' = fold Inttab.delete canceled execs; |
88 in SOME ((), (context, execs')) end); |
81 in SOME ((), (execution_id, execs')) end); |
89 |
82 |
90 fun terminate_all () = |
83 fun terminate_all () = |
91 let |
84 let |
92 val groups = |
85 val groups = |
93 Inttab.fold (fn (_, SOME group) => cons group | _ => I) |
86 Inttab.fold (fn (_, SOME group) => cons group | _ => I) |