equal
deleted
inserted
replaced
1 (* Title: Pure/PIDE/execution.ML |
1 (* Title: Pure/PIDE/execution.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Global management of execution. Unique running execution serves as |
4 Global management of execution. Unique running execution serves as |
5 barrier for further exploration of exec particles. |
5 barrier for further exploration of exec fragments. |
6 *) |
6 *) |
7 |
7 |
8 signature EXECUTION = |
8 signature EXECUTION = |
9 sig |
9 sig |
10 val start: unit -> Document_ID.execution |
10 val start: unit -> Document_ID.execution |
53 in SOME (continue, (execution_id', execs')) end); |
53 in SOME (continue, (execution_id', execs')) end); |
54 |
54 |
55 fun finished exec_id = |
55 fun finished exec_id = |
56 Synchronized.change state |
56 Synchronized.change state |
57 (apsnd (fn execs => |
57 (apsnd (fn execs => |
58 Inttab.delete exec_id execs |
58 Inttab.delete exec_id execs handle Inttab.UNDEF bad => |
59 handle Inttab.UNDEF bad => |
59 error ("Attempt to finish unknown execution " ^ Document_ID.print bad))); |
60 error ("Attempt to finish unknown execution: " ^ Document_ID.print bad))); |
|
61 |
60 |
62 fun peek exec_id = |
61 fun peek exec_id = |
63 Inttab.lookup (snd (Synchronized.value state)) exec_id; |
62 Inttab.lookup (snd (Synchronized.value state)) exec_id; |
64 |
63 |
65 fun snapshot () = |
64 fun snapshot () = |