author | wenzelm |
Mon, 15 Jul 2013 10:31:41 +0200 | |
changeset 52656 | 9437f440ef3f |
parent 52651 | 5adb5c69af97 |
child 52657 | 42c14dba1daa |
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 |
|
52600 | 9 |
val read: (unit -> theory) -> Token.T list -> Toplevel.transition |
10 |
type eval |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
11 |
val eval_eq: eval * eval -> bool |
52536 | 12 |
val eval_result_state: eval -> Toplevel.state |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
13 |
val eval_stable: eval -> bool |
52535
b7badd371e4d
tuned signature -- eliminated pointless type synonym;
wenzelm
parents:
52534
diff
changeset
|
14 |
val eval: (unit -> theory) -> Token.T list -> eval -> eval |
52600 | 15 |
type print |
52570 | 16 |
val print: bool -> string -> eval -> print list -> print list option |
52526 | 17 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit |
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
18 |
val print_function: string -> |
52651 | 19 |
({command_name: string} -> |
20 |
{delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit |
|
52571 | 21 |
val no_print_function: string -> unit |
52600 | 22 |
type exec = eval * print list |
23 |
val no_exec: exec |
|
24 |
val exec_ids: exec option -> Document_ID.exec list |
|
52606 | 25 |
val exec: Document_ID.execution -> exec -> unit |
47336 | 26 |
end; |
27 |
||
28 |
structure Command: COMMAND = |
|
29 |
struct |
|
30 |
||
52534 | 31 |
(** memo results -- including physical interrupts! **) |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
32 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
33 |
datatype 'a expr = |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
34 |
Expr of Document_ID.exec * (unit -> 'a) | |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
35 |
Result of 'a Exn.result; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
36 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
37 |
abstype 'a memo = Memo of 'a expr Synchronized.var |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
38 |
with |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
39 |
|
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
40 |
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
|
41 |
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
|
42 |
|
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
43 |
fun memo_result (Memo v) = |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
44 |
(case Synchronized.value v of |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
45 |
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
|
46 |
| Result res => Exn.release res); |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
47 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
48 |
fun memo_stable (Memo v) = |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
49 |
(case Synchronized.value v of |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
50 |
Expr _ => true |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
51 |
| Result res => not (Exn.is_interrupt_exn res)); |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
52 |
|
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
53 |
fun memo_finished (Memo v) = |
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
54 |
(case Synchronized.value v of |
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
55 |
Expr _ => false |
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
56 |
| Result res => not (Exn.is_interrupt_exn res)); |
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) = |
52609
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
59 |
Synchronized.guarded_access v |
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 |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
62 |
Result res => SOME (res, expr) |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
63 |
| Expr (exec_id, e) => |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
64 |
uninterruptible (fn restore_attributes => fn () => |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
65 |
if Execution.running execution_id exec_id then |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
66 |
let |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
67 |
val res = Exn.capture (restore_attributes e) (); |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
68 |
val _ = Execution.finished exec_id; |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
69 |
in SOME (res, Result res) end |
c8f8c29193de
clarified memo_exec: plain synchronized access without any special tricks;
wenzelm
parents:
52607
diff
changeset
|
70 |
else SOME (Exn.interrupt_exn, expr)) ())) |
52604 | 71 |
|> Exn.release |> ignore; |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
72 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
73 |
fun memo_fork params execution_id (Memo v) = |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
74 |
(case Synchronized.value v of |
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
75 |
Result _ => () |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
76 |
| _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v)))); |
52526 | 77 |
|
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
78 |
end; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
79 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
80 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
81 |
|
52536 | 82 |
(** main phases of execution **) |
83 |
||
52510 | 84 |
(* read *) |
52509 | 85 |
|
52534 | 86 |
fun read init span = |
52510 | 87 |
let |
88 |
val outer_syntax = #2 (Outer_Syntax.get_syntax ()); |
|
89 |
val command_reports = Outer_Syntax.command_reports outer_syntax; |
|
52509 | 90 |
|
52534 | 91 |
val proper_range = |
92 |
Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span))); |
|
52510 | 93 |
val pos = |
94 |
(case find_first Token.is_command span of |
|
95 |
SOME tok => Token.position_of tok |
|
96 |
| NONE => proper_range); |
|
52509 | 97 |
|
52510 | 98 |
val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span; |
99 |
val _ = Position.reports_text (token_reports @ maps command_reports span); |
|
100 |
in |
|
101 |
if is_malformed then Toplevel.malformed pos "Malformed command syntax" |
|
102 |
else |
|
103 |
(case Outer_Syntax.read_spans outer_syntax span of |
|
104 |
[tr] => |
|
105 |
if Keyword.is_control (Toplevel.name_of tr) then |
|
106 |
Toplevel.malformed pos "Illegal control command" |
|
52534 | 107 |
else Toplevel.modify_init init tr |
108 |
| [] => Toplevel.ignored (Position.set_range (Token.position_range_of span)) |
|
52510 | 109 |
| _ => Toplevel.malformed proper_range "Exactly one command expected") |
110 |
handle ERROR msg => Toplevel.malformed proper_range msg |
|
111 |
end; |
|
52509 | 112 |
|
113 |
||
114 |
(* eval *) |
|
47336 | 115 |
|
52600 | 116 |
type eval_state = |
117 |
{failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}; |
|
118 |
val init_eval_state = |
|
119 |
{failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; |
|
120 |
||
121 |
datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo}; |
|
122 |
||
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
123 |
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
|
124 |
|
52600 | 125 |
fun eval_result (Eval {eval_process, ...}) = memo_result eval_process; |
126 |
val eval_result_state = #state o eval_result; |
|
127 |
||
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
128 |
fun eval_stable (Eval {exec_id, eval_process}) = |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
129 |
Goal.stable_futures exec_id andalso memo_stable eval_process; |
52600 | 130 |
|
47336 | 131 |
local |
132 |
||
133 |
fun run int tr st = |
|
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51266
diff
changeset
|
134 |
if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then |
51605
eca8acb42e4a
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents:
51603
diff
changeset
|
135 |
(Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} |
eca8acb42e4a
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents:
51603
diff
changeset
|
136 |
(fn () => Toplevel.command_exception int tr st); ([], SOME st)) |
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51266
diff
changeset
|
137 |
else Toplevel.command_errors int tr st; |
47336 | 138 |
|
52510 | 139 |
fun check_cmts span tr st' = |
140 |
Toplevel.setmp_thread_position tr |
|
141 |
(fn () => |
|
142 |
Outer_Syntax.side_comments span |> maps (fn cmt => |
|
143 |
(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
|
144 |
handle exn => |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
145 |
if Exn.is_interrupt exn then reraise exn |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
146 |
else ML_Compiler.exn_messages_ids exn)) (); |
52510 | 147 |
|
47336 | 148 |
fun proof_status tr st = |
149 |
(case try Toplevel.proof_of st of |
|
150 |
SOME prf => Toplevel.status tr (Proof.status_markup prf) |
|
151 |
| NONE => ()); |
|
152 |
||
52534 | 153 |
fun eval_state span tr ({malformed, state = st, ...}: eval_state) = |
52509 | 154 |
if malformed then |
52526 | 155 |
{failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel} |
48772 | 156 |
else |
157 |
let |
|
158 |
val malformed' = Toplevel.is_malformed tr; |
|
159 |
val is_init = Toplevel.is_init tr; |
|
160 |
val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
|
47336 | 161 |
|
48772 | 162 |
val _ = Multithreading.interrupted (); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49866
diff
changeset
|
163 |
val _ = Toplevel.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
|
164 |
val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
52509 | 165 |
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
|
166 |
val errs = errs1 @ errs2; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49866
diff
changeset
|
167 |
val _ = Toplevel.status tr Markup.finished; |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
168 |
val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; |
48772 | 169 |
in |
170 |
(case result of |
|
171 |
NONE => |
|
172 |
let |
|
173 |
val _ = if null errs then Exn.interrupt () else (); |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49866
diff
changeset
|
174 |
val _ = Toplevel.status tr Markup.failed; |
52526 | 175 |
in {failed = true, malformed = malformed', command = tr, state = st} end |
48772 | 176 |
| SOME st' => |
177 |
let |
|
178 |
val _ = proof_status tr st'; |
|
52526 | 179 |
in {failed = false, malformed = malformed', command = tr, state = st'} end) |
48772 | 180 |
end; |
47336 | 181 |
|
52534 | 182 |
in |
183 |
||
184 |
fun eval init span eval0 = |
|
185 |
let |
|
186 |
val exec_id = Document_ID.make (); |
|
187 |
fun process () = |
|
188 |
let |
|
189 |
val tr = |
|
190 |
Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) |
|
52536 | 191 |
(fn () => read init span |> Toplevel.exec_id exec_id) (); |
52534 | 192 |
in eval_state span tr (eval_result eval0) end; |
52600 | 193 |
in Eval {exec_id = exec_id, eval_process = memo exec_id process} end; |
52534 | 194 |
|
47336 | 195 |
end; |
196 |
||
52509 | 197 |
|
198 |
(* print *) |
|
199 |
||
52600 | 200 |
datatype print = Print of |
52651 | 201 |
{name: string, delay: Time.time, pri: int, persistent: bool, |
52600 | 202 |
exec_id: Document_ID.exec, print_process: unit memo}; |
203 |
||
52526 | 204 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit; |
52515 | 205 |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
206 |
type print_function = |
52651 | 207 |
{command_name: string} -> |
208 |
{delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option; |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
209 |
|
52511 | 210 |
local |
211 |
||
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
212 |
val print_functions = |
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
213 |
Synchronized.var "Command.print_functions" ([]: (string * print_function) list); |
52511 | 214 |
|
52570 | 215 |
fun print_error tr e = |
52619
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
216 |
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
217 |
handle exn => |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
218 |
if Exn.is_interrupt exn then reraise exn |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
219 |
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
|
220 |
|
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
221 |
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
|
222 |
|
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
223 |
fun print_stable (Print {exec_id, print_process, ...}) = |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
224 |
Goal.stable_futures exec_id andalso memo_stable print_process; |
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
225 |
|
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
226 |
fun print_finished (Print {exec_id, print_process, ...}) = |
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
227 |
Goal.stable_futures exec_id andalso memo_finished print_process; |
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
228 |
|
52600 | 229 |
fun print_persistent (Print {persistent, ...}) = persistent; |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
230 |
|
52511 | 231 |
in |
52509 | 232 |
|
52570 | 233 |
fun print command_visible command_name eval old_prints = |
234 |
let |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
235 |
fun new_print (name, get_pr) = |
52570 | 236 |
let |
52651 | 237 |
fun make_print strict {delay, pri, persistent, print_fn} = |
52570 | 238 |
let |
239 |
val exec_id = Document_ID.make (); |
|
240 |
fun process () = |
|
241 |
let |
|
242 |
val {failed, command, state = st', ...} = eval_result eval; |
|
243 |
val tr = Toplevel.exec_id exec_id command; |
|
244 |
in |
|
245 |
if failed andalso not strict then () |
|
246 |
else print_error tr (fn () => print_fn tr st') |
|
247 |
end; |
|
52572
2fb1f9cf80d3
print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;
wenzelm
parents:
52571
diff
changeset
|
248 |
in |
52600 | 249 |
Print { |
52651 | 250 |
name = name, delay = delay, pri = pri, persistent = persistent, |
52600 | 251 |
exec_id = exec_id, print_process = memo exec_id process} |
52572
2fb1f9cf80d3
print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;
wenzelm
parents:
52571
diff
changeset
|
252 |
end; |
52570 | 253 |
in |
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
254 |
(case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of |
52570 | 255 |
Exn.Res NONE => NONE |
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
256 |
| Exn.Res (SOME pr) => SOME (make_print false pr) |
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
257 |
| Exn.Exn exn => |
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
258 |
SOME (make_print true |
52651 | 259 |
{delay = Time.zeroTime, pri = 0, persistent = false, |
260 |
print_fn = fn _ => fn _ => reraise exn})) |
|
52570 | 261 |
end; |
262 |
||
263 |
val new_prints = |
|
264 |
if command_visible then |
|
265 |
rev (Synchronized.value print_functions) |> map_filter (fn pr => |
|
52600 | 266 |
(case find_first (fn Print {name, ...} => name = fst pr) old_prints of |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
267 |
SOME print => if print_stable print then SOME print else new_print pr |
52570 | 268 |
| NONE => new_print pr)) |
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
269 |
else filter (fn print => print_finished print andalso print_persistent print) old_prints; |
52570 | 270 |
in |
52600 | 271 |
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints |
52570 | 272 |
end; |
52511 | 273 |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
274 |
fun print_function name f = |
52511 | 275 |
Synchronized.change print_functions (fn funs => |
276 |
(if not (AList.defined (op =) funs name) then () |
|
277 |
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
|
278 |
AList.update (op =) (name, f) funs)); |
52511 | 279 |
|
52571 | 280 |
fun no_print_function name = |
281 |
Synchronized.change print_functions (filter_out (equal name o #1)); |
|
282 |
||
52511 | 283 |
end; |
284 |
||
52526 | 285 |
val _ = |
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
286 |
print_function "print_state" |
52651 | 287 |
(fn {command_name} => |
288 |
SOME {delay = Time.zeroTime, pri = 0, persistent = true, |
|
289 |
print_fn = fn tr => fn st' => |
|
290 |
let |
|
291 |
val is_init = Keyword.is_theory_begin command_name; |
|
292 |
val is_proof = Keyword.is_proof command_name; |
|
293 |
val do_print = |
|
294 |
not is_init andalso |
|
295 |
(Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); |
|
296 |
in if do_print then Toplevel.print_state false st' else () end}); |
|
52509 | 297 |
|
52532 | 298 |
|
52600 | 299 |
(* combined execution *) |
300 |
||
301 |
type exec = eval * print list; |
|
302 |
val no_exec: exec = |
|
303 |
(Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); |
|
52532 | 304 |
|
52600 | 305 |
fun exec_ids NONE = [] |
306 |
| exec_ids (SOME (Eval {exec_id, ...}, prints)) = |
|
307 |
exec_id :: map (fn Print {exec_id, ...} => exec_id) prints; |
|
308 |
||
309 |
local |
|
310 |
||
52651 | 311 |
fun run_print execution_id (Print {name, delay, pri, print_process, ...}) = |
312 |
if Multithreading.enabled () then |
|
313 |
let |
|
314 |
val group = Future.worker_subgroup (); |
|
315 |
fun fork () = |
|
316 |
memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true} |
|
317 |
execution_id print_process; |
|
318 |
in |
|
319 |
if delay = Time.zeroTime then fork () |
|
320 |
else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork) |
|
321 |
end |
|
322 |
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
|
323 |
|
52600 | 324 |
in |
325 |
||
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
326 |
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
|
327 |
(memo_exec execution_id eval_process; List.app (run_print execution_id) prints); |
52532 | 328 |
|
47336 | 329 |
end; |
330 |
||
52600 | 331 |
end; |
332 |