author | wenzelm |
Thu, 27 Feb 2014 17:29:58 +0100 | |
changeset 55788 | 67699e08e969 |
parent 55709 | 4e5a83a46ded |
child 55798 | 985bd3a325ab |
permissions | -rw-r--r-- |
47336 | 1 |
(* Title: Pure/PIDE/command.ML |
2 |
Author: Makarius |
|
3 |
||
52534 | 4 |
Prover command execution: read -- eval -- print. |
47336 | 5 |
*) |
6 |
||
7 |
signature COMMAND = |
|
8 |
sig |
|
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
9 |
type 'a blob = (string * 'a option) Exn.result |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
10 |
type blob_digest = string blob |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
11 |
type content = SHA1.digest * string list |
54526 | 12 |
val read_file: Path.T -> Position.T -> Path.T -> Token.file |
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
13 |
val read: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> Toplevel.transition |
52600 | 14 |
type eval |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
15 |
val eval_eq: eval * eval -> bool |
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52775
diff
changeset
|
16 |
val eval_running: eval -> bool |
52772 | 17 |
val eval_finished: eval -> bool |
52536 | 18 |
val eval_result_state: eval -> Toplevel.state |
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
19 |
val eval: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> eval -> eval |
52600 | 20 |
type print |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
21 |
val print: bool -> (string * string list) list -> string -> |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
22 |
eval -> print list -> print list option |
52526 | 23 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit |
52953
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
24 |
type print_function = |
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
25 |
{command_name: string, args: string list} -> |
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
26 |
{delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option |
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
27 |
val print_function: string -> print_function -> unit |
52571 | 28 |
val no_print_function: string -> unit |
52600 | 29 |
type exec = eval * print list |
30 |
val no_exec: exec |
|
31 |
val exec_ids: exec option -> Document_ID.exec list |
|
52606 | 32 |
val exec: Document_ID.execution -> exec -> unit |
47336 | 33 |
end; |
34 |
||
35 |
structure Command: COMMAND = |
|
36 |
struct |
|
37 |
||
52775
e0169f13bd37
keep memo_exec execution running, which is important to cancel goal forks eventually;
wenzelm
parents:
52774
diff
changeset
|
38 |
(** memo results **) |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
39 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
40 |
datatype 'a expr = |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
41 |
Expr of Document_ID.exec * (unit -> 'a) | |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
42 |
Result of 'a Exn.result; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
43 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
44 |
abstype 'a memo = Memo of 'a expr Synchronized.var |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
45 |
with |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
46 |
|
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
47 |
fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e))); |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
48 |
fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a))); |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
49 |
|
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
50 |
fun memo_result (Memo v) = |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
51 |
(case Synchronized.value v of |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
52 |
Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id) |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
53 |
| Result res => Exn.release res); |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
54 |
|
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
55 |
fun memo_finished (Memo v) = |
52785 | 56 |
(case Synchronized.value v of Expr _ => false | Result _ => true); |
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
57 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
58 |
fun memo_exec execution_id (Memo v) = |
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
59 |
Synchronized.timed_access v (K (SOME Time.zeroTime)) |
52609
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
60 |
(fn expr => |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
61 |
(case expr of |
52775
e0169f13bd37
keep memo_exec execution running, which is important to cancel goal forks eventually;
wenzelm
parents:
52774
diff
changeset
|
62 |
Expr (exec_id, body) => |
52609
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
63 |
uninterruptible (fn restore_attributes => fn () => |
54637
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
64 |
let val group = Future.worker_subgroup () in |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
65 |
if Execution.running execution_id exec_id [group] then |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
66 |
let |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
67 |
val res = |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
68 |
(body |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
69 |
|> restore_attributes |
54649
99b9249b3e05
more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
wenzelm
parents:
54647
diff
changeset
|
70 |
|> Future.task_context "Command.memo_exec" group |
54637
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
71 |
|> Exn.interruptible_capture) (); |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
72 |
in SOME ((), Result res) end |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
73 |
else SOME ((), expr) |
db3d3d99c69d
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
wenzelm
parents:
53976
diff
changeset
|
74 |
end) () |
52775
e0169f13bd37
keep memo_exec execution running, which is important to cancel goal forks eventually;
wenzelm
parents:
52774
diff
changeset
|
75 |
| Result _ => SOME ((), expr))) |
e0169f13bd37
keep memo_exec execution running, which is important to cancel goal forks eventually;
wenzelm
parents:
52774
diff
changeset
|
76 |
|> (fn NONE => error "Conflicting command execution" | _ => ()); |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
77 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
78 |
fun memo_fork params execution_id (Memo v) = |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
79 |
(case Synchronized.value v of |
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
80 |
Result _ => () |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
81 |
| _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v)))); |
52526 | 82 |
|
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
83 |
end; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
84 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
85 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
86 |
|
52536 | 87 |
(** main phases of execution **) |
88 |
||
52510 | 89 |
(* read *) |
52509 | 90 |
|
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
91 |
type 'a blob = (string * 'a option) Exn.result; (*file node name, content*) |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
92 |
type blob_digest = string blob; (*raw digest*) |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
93 |
type content = SHA1.digest * string list; (*digest, lines*) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
94 |
|
54526 | 95 |
fun read_file master_dir pos src_path = |
96 |
let |
|
97 |
val full_path = File.check_file (File.full_path master_dir src_path); |
|
98 |
val _ = Position.report pos (Markup.path (Path.implode full_path)); |
|
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
99 |
val text = File.read full_path; |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
100 |
val lines = split_lines text; |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
101 |
val digest = SHA1.digest text; |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
102 |
in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end; |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
103 |
|
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
104 |
local |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
105 |
|
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
106 |
fun blob_file src_path file (digest, lines) = |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
107 |
let |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
108 |
val file_pos = |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
109 |
Position.file file (*sic!*) |> |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
110 |
(case Position.get_id (Position.thread_data ()) of |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
111 |
NONE => I |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
112 |
| SOME exec_id => Position.put_id exec_id); |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
113 |
in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end |
54526 | 114 |
|
115 |
fun resolve_files master_dir blobs toks = |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
116 |
(case Thy_Syntax.parse_spans toks of |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
117 |
[span] => span |
54523 | 118 |
|> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) => |
119 |
let |
|
54526 | 120 |
fun make_file src_path (Exn.Res (_, NONE)) = |
121 |
Exn.interruptible_capture (fn () => read_file master_dir pos src_path) () |
|
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
122 |
| make_file src_path (Exn.Res (file, SOME content)) = |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
123 |
(Position.report pos (Markup.path file); |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
124 |
Exn.Res (blob_file src_path file content)) |
54523 | 125 |
| make_file _ (Exn.Exn e) = Exn.Exn e; |
126 |
val src_paths = Keyword.command_files cmd path; |
|
127 |
in |
|
54527
bfeb0ea6c2c0
proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;
wenzelm
parents:
54526
diff
changeset
|
128 |
if null blobs then |
bfeb0ea6c2c0
proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;
wenzelm
parents:
54526
diff
changeset
|
129 |
map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) |
bfeb0ea6c2c0
proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;
wenzelm
parents:
54526
diff
changeset
|
130 |
else if length src_paths = length blobs then |
bfeb0ea6c2c0
proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;
wenzelm
parents:
54526
diff
changeset
|
131 |
map2 make_file src_paths blobs |
bfeb0ea6c2c0
proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;
wenzelm
parents:
54526
diff
changeset
|
132 |
else error ("Misalignment of inlined files" ^ Position.here pos) |
54523 | 133 |
end) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
134 |
|> Thy_Syntax.span_content |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
135 |
| _ => toks); |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
136 |
|
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
137 |
in |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
138 |
|
54526 | 139 |
fun read init master_dir blobs span = |
52510 | 140 |
let |
141 |
val outer_syntax = #2 (Outer_Syntax.get_syntax ()); |
|
142 |
val command_reports = Outer_Syntax.command_reports outer_syntax; |
|
52509 | 143 |
|
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
144 |
val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span)); |
52510 | 145 |
val pos = |
146 |
(case find_first Token.is_command span of |
|
55708 | 147 |
SOME tok => Token.pos_of tok |
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
148 |
| NONE => #1 proper_range); |
52509 | 149 |
|
52510 | 150 |
val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span; |
151 |
val _ = Position.reports_text (token_reports @ maps command_reports span); |
|
152 |
in |
|
153 |
if is_malformed then Toplevel.malformed pos "Malformed command syntax" |
|
154 |
else |
|
54526 | 155 |
(case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of |
52510 | 156 |
[tr] => |
157 |
if Keyword.is_control (Toplevel.name_of tr) then |
|
158 |
Toplevel.malformed pos "Illegal control command" |
|
52534 | 159 |
else Toplevel.modify_init init tr |
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
160 |
| [] => Toplevel.ignored (#1 (Token.range_of span)) |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
161 |
| _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected") |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
162 |
handle ERROR msg => Toplevel.malformed (#1 proper_range) msg |
52510 | 163 |
end; |
52509 | 164 |
|
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
165 |
end; |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55709
diff
changeset
|
166 |
|
52509 | 167 |
|
168 |
(* eval *) |
|
47336 | 169 |
|
52600 | 170 |
type eval_state = |
171 |
{failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}; |
|
172 |
val init_eval_state = |
|
173 |
{failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; |
|
174 |
||
175 |
datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo}; |
|
176 |
||
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
177 |
fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id'; |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
178 |
|
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52775
diff
changeset
|
179 |
fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id; |
52772 | 180 |
fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process; |
181 |
||
52600 | 182 |
fun eval_result (Eval {eval_process, ...}) = memo_result eval_process; |
183 |
val eval_result_state = #state o eval_result; |
|
184 |
||
47336 | 185 |
local |
186 |
||
187 |
fun run int tr st = |
|
53189
ee8b8dafef0e
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents:
52999
diff
changeset
|
188 |
if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then |
53192 | 189 |
(Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} |
51605
eca8acb42e4a
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents:
51603
diff
changeset
|
190 |
(fn () => Toplevel.command_exception int tr st); ([], SOME st)) |
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51266
diff
changeset
|
191 |
else Toplevel.command_errors int tr st; |
47336 | 192 |
|
52510 | 193 |
fun check_cmts span tr st' = |
194 |
Toplevel.setmp_thread_position tr |
|
195 |
(fn () => |
|
196 |
Outer_Syntax.side_comments span |> maps (fn cmt => |
|
197 |
(Thy_Output.check_text (Token.source_position_of cmt) st'; []) |
|
52619
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
198 |
handle exn => |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
199 |
if Exn.is_interrupt exn then reraise exn |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
200 |
else ML_Compiler.exn_messages_ids exn)) (); |
52510 | 201 |
|
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
202 |
fun report tr m = |
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
203 |
Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) (); |
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
204 |
|
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
205 |
fun status tr m = |
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
206 |
Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); |
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
207 |
|
47336 | 208 |
fun proof_status tr st = |
209 |
(case try Toplevel.proof_of st of |
|
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
210 |
SOME prf => status tr (Proof.status_markup prf) |
47336 | 211 |
| NONE => ()); |
212 |
||
52534 | 213 |
fun eval_state span tr ({malformed, state = st, ...}: eval_state) = |
52509 | 214 |
if malformed then |
52526 | 215 |
{failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel} |
48772 | 216 |
else |
217 |
let |
|
218 |
val malformed' = Toplevel.is_malformed tr; |
|
219 |
val is_init = Toplevel.is_init tr; |
|
220 |
val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
|
47336 | 221 |
|
48772 | 222 |
val _ = Multithreading.interrupted (); |
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
223 |
val _ = status tr Markup.running; |
48918
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48772
diff
changeset
|
224 |
val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
52509 | 225 |
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); |
48918
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48772
diff
changeset
|
226 |
val errs = errs1 @ errs2; |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
227 |
val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; |
48772 | 228 |
in |
229 |
(case result of |
|
230 |
NONE => |
|
231 |
let |
|
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
232 |
val _ = status tr Markup.failed; |
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
233 |
val _ = status tr Markup.finished; |
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
234 |
val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else (); |
52526 | 235 |
in {failed = true, malformed = malformed', command = tr, state = st} end |
48772 | 236 |
| SOME st' => |
237 |
let |
|
238 |
val _ = proof_status tr st'; |
|
54678
87910da843d5
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents:
54671
diff
changeset
|
239 |
val _ = status tr Markup.finished; |
52526 | 240 |
in {failed = false, malformed = malformed', command = tr, state = st'} end) |
48772 | 241 |
end; |
47336 | 242 |
|
52534 | 243 |
in |
244 |
||
54526 | 245 |
fun eval init master_dir blobs span eval0 = |
52534 | 246 |
let |
247 |
val exec_id = Document_ID.make (); |
|
248 |
fun process () = |
|
249 |
let |
|
250 |
val tr = |
|
251 |
Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) |
|
54526 | 252 |
(fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) (); |
52534 | 253 |
in eval_state span tr (eval_result eval0) end; |
52600 | 254 |
in Eval {exec_id = exec_id, eval_process = memo exec_id process} end; |
52534 | 255 |
|
47336 | 256 |
end; |
257 |
||
52509 | 258 |
|
259 |
(* print *) |
|
260 |
||
52600 | 261 |
datatype print = Print of |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
262 |
{name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, |
52600 | 263 |
exec_id: Document_ID.exec, print_process: unit memo}; |
264 |
||
52526 | 265 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit; |
52515 | 266 |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
267 |
type print_function = |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
268 |
{command_name: string, args: string list} -> |
52953
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
269 |
{delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option; |
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
270 |
|
52511 | 271 |
local |
272 |
||
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
273 |
val print_functions = |
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
274 |
Synchronized.var "Command.print_functions" ([]: (string * print_function) list); |
52511 | 275 |
|
52570 | 276 |
fun print_error tr e = |
53709
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
53404
diff
changeset
|
277 |
(Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e () |
52619
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
278 |
handle exn => |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
279 |
if Exn.is_interrupt exn then reraise exn |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
280 |
else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); |
52516
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
281 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
282 |
fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id'; |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
283 |
|
52775
e0169f13bd37
keep memo_exec execution running, which is important to cancel goal forks eventually;
wenzelm
parents:
52774
diff
changeset
|
284 |
fun print_finished (Print {print_process, ...}) = memo_finished print_process; |
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
285 |
|
52600 | 286 |
fun print_persistent (Print {persistent, ...}) = persistent; |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
287 |
|
52853
4ab66773a41f
prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents:
52850
diff
changeset
|
288 |
val overlay_ord = prod_ord string_ord (list_ord string_ord); |
4ab66773a41f
prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents:
52850
diff
changeset
|
289 |
|
52511 | 290 |
in |
52509 | 291 |
|
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
292 |
fun print command_visible command_overlays command_name eval old_prints = |
52570 | 293 |
let |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
294 |
val print_functions = Synchronized.value print_functions; |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
295 |
|
52999
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
296 |
fun make_print name args {delay, pri, persistent, strict, print_fn} = |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
297 |
let |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
298 |
val exec_id = Document_ID.make (); |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
299 |
fun process () = |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
300 |
let |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
301 |
val {failed, command, state = st', ...} = eval_result eval; |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
302 |
val tr = Toplevel.exec_id exec_id command; |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
303 |
in |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
304 |
if failed andalso strict then () |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
305 |
else print_error tr (fn () => print_fn tr st') |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
306 |
end; |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
307 |
in |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
308 |
Print { |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
309 |
name = name, args = args, delay = delay, pri = pri, persistent = persistent, |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
310 |
exec_id = exec_id, print_process = memo exec_id process} |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
311 |
end; |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
312 |
|
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
313 |
fun bad_print name args exn = |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
314 |
make_print name args {delay = NONE, pri = 0, persistent = false, |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
315 |
strict = false, print_fn = fn _ => fn _ => reraise exn}; |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
316 |
|
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
317 |
fun new_print name args get_pr = |
52570 | 318 |
let |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
319 |
val params = {command_name = command_name, args = args}; |
52570 | 320 |
in |
53709
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
53404
diff
changeset
|
321 |
(case Exn.capture (Toplevel.controlled_execution get_pr) params of |
52570 | 322 |
Exn.Res NONE => NONE |
52999
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
323 |
| Exn.Res (SOME pr) => SOME (make_print name args pr) |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
324 |
| Exn.Exn exn => SOME (bad_print name args exn)) |
52570 | 325 |
end; |
326 |
||
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
327 |
fun get_print (a, b) = |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
328 |
(case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
329 |
NONE => |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
330 |
(case AList.lookup (op =) print_functions a of |
52999
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
331 |
NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a))) |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
332 |
| SOME get_pr => new_print a b get_pr) |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
333 |
| some => some); |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
334 |
|
52570 | 335 |
val new_prints = |
336 |
if command_visible then |
|
52853
4ab66773a41f
prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents:
52850
diff
changeset
|
337 |
fold (fn (a, _) => cons (a, [])) print_functions command_overlays |
4ab66773a41f
prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents:
52850
diff
changeset
|
338 |
|> sort_distinct overlay_ord |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
339 |
|> map_filter get_print |
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
340 |
else filter (fn print => print_finished print andalso print_persistent print) old_prints; |
52570 | 341 |
in |
52600 | 342 |
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints |
52570 | 343 |
end; |
52511 | 344 |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
345 |
fun print_function name f = |
52511 | 346 |
Synchronized.change print_functions (fn funs => |
347 |
(if not (AList.defined (op =) funs name) then () |
|
348 |
else warning ("Redefining command print function: " ^ quote name); |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
349 |
AList.update (op =) (name, f) funs)); |
52511 | 350 |
|
52571 | 351 |
fun no_print_function name = |
352 |
Synchronized.change print_functions (filter_out (equal name o #1)); |
|
353 |
||
52511 | 354 |
end; |
355 |
||
52526 | 356 |
val _ = |
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
357 |
print_function "print_state" |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
358 |
(fn {command_name, ...} => |
53404
d598b6231ff7
non-persistent print_state: trade-off between JVM space vs. ML time;
wenzelm
parents:
53375
diff
changeset
|
359 |
SOME {delay = NONE, pri = 1, persistent = false, strict = true, |
52651 | 360 |
print_fn = fn tr => fn st' => |
361 |
let |
|
362 |
val is_init = Keyword.is_theory_begin command_name; |
|
363 |
val is_proof = Keyword.is_proof command_name; |
|
364 |
val do_print = |
|
365 |
not is_init andalso |
|
366 |
(Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); |
|
367 |
in if do_print then Toplevel.print_state false st' else () end}); |
|
52509 | 368 |
|
52532 | 369 |
|
52600 | 370 |
(* combined execution *) |
371 |
||
372 |
type exec = eval * print list; |
|
373 |
val no_exec: exec = |
|
374 |
(Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); |
|
52532 | 375 |
|
52600 | 376 |
fun exec_ids NONE = [] |
377 |
| exec_ids (SOME (Eval {exec_id, ...}, prints)) = |
|
378 |
exec_id :: map (fn Print {exec_id, ...} => exec_id) prints; |
|
379 |
||
380 |
local |
|
381 |
||
52651 | 382 |
fun run_print execution_id (Print {name, delay, pri, print_process, ...}) = |
53976
da610b507799
low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
wenzelm
parents:
53709
diff
changeset
|
383 |
if Multithreading.enabled () orelse pri <= 0 then |
52651 | 384 |
let |
385 |
val group = Future.worker_subgroup (); |
|
386 |
fun fork () = |
|
387 |
memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true} |
|
388 |
execution_id print_process; |
|
389 |
in |
|
52762 | 390 |
(case delay of |
391 |
NONE => fork () |
|
392 |
| SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork)) |
|
52651 | 393 |
end |
394 |
else memo_exec execution_id print_process; |
|
52559
ddaf277e0d8c
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents:
52536
diff
changeset
|
395 |
|
52600 | 396 |
in |
397 |
||
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
398 |
fun exec execution_id (Eval {eval_process, ...}, prints) = |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
399 |
(memo_exec execution_id eval_process; List.app (run_print execution_id) prints); |
52532 | 400 |
|
47336 | 401 |
end; |
402 |
||
52600 | 403 |
end; |
404 |