author | wenzelm |
Fri, 09 Oct 2015 21:16:00 +0200 | |
changeset 61379 | c57820ceead3 |
parent 61213 | 0b1a092385c7 |
child 61457 | 3e21699bb83b |
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 |
|
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
9 |
type blob = (string * (SHA1.digest * string list) option) Exn.result |
54526 | 10 |
val read_file: Path.T -> Position.T -> Path.T -> Token.file |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
11 |
val read_thy: Toplevel.state -> theory |
58934
385a4cc7426f
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
wenzelm
parents:
58928
diff
changeset
|
12 |
val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
13 |
blob list * int -> 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 |
58934
385a4cc7426f
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
wenzelm
parents:
58928
diff
changeset
|
19 |
val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
20 |
blob list * int -> Token.T list -> eval -> eval |
52600 | 21 |
type print |
58923 | 22 |
val print: bool -> (string * string list) list -> Keyword.keywords -> string -> |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
23 |
eval -> print list -> print list option |
52526 | 24 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit |
52953
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
25 |
type print_function = |
58923 | 26 |
{keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> |
52953
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
27 |
{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
|
28 |
val print_function: string -> print_function -> unit |
52571 | 29 |
val no_print_function: string -> unit |
52600 | 30 |
type exec = eval * print list |
31 |
val no_exec: exec |
|
32 |
val exec_ids: exec option -> Document_ID.exec list |
|
52606 | 33 |
val exec: Document_ID.execution -> exec -> unit |
47336 | 34 |
end; |
35 |
||
36 |
structure Command: COMMAND = |
|
37 |
struct |
|
38 |
||
52536 | 39 |
(** main phases of execution **) |
40 |
||
59466
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
41 |
fun task_context group f = |
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
42 |
f |
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
43 |
|> Future.interruptible_task |
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
44 |
|> Future.task_context "Command.run_process" group; |
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
45 |
|
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
46 |
|
52510 | 47 |
(* read *) |
52509 | 48 |
|
55798 | 49 |
type blob = |
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
50 |
(string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
51 |
|
56504
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
52 |
fun read_file_node file_node master_dir pos src_path = |
54526 | 53 |
let |
59944
83071f4c8ae6
recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
wenzelm
parents:
59809
diff
changeset
|
54 |
val _ = Position.report pos Markup.language_path; |
56504
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
55 |
val _ = |
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
56 |
(case try Url.explode file_node of |
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
57 |
NONE => () |
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
58 |
| SOME (Url.File _) => () |
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
59 |
| _ => |
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
60 |
error ("Prover cannot load remote file " ^ |
59685
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59472
diff
changeset
|
61 |
Markup.markup (Markup.path file_node) (quote file_node))); |
54526 | 62 |
val full_path = File.check_file (File.full_path master_dir 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
|
63 |
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
|
64 |
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
|
65 |
val digest = SHA1.digest text; |
59685
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59472
diff
changeset
|
66 |
in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end |
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59472
diff
changeset
|
67 |
handle ERROR msg => error (msg ^ Position.here pos); |
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
|
68 |
|
56504
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
69 |
val read_file = read_file_node ""; |
d71f4be7e287
tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents:
56458
diff
changeset
|
70 |
|
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
|
71 |
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
|
72 |
|
56447
1e77ed11f2f7
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents:
56333
diff
changeset
|
73 |
fun blob_file src_path lines digest file_node = |
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
|
74 |
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
|
75 |
val file_pos = |
56447
1e77ed11f2f7
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents:
56333
diff
changeset
|
76 |
Position.file file_node |> |
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
|
77 |
(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
|
78 |
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
|
79 |
| 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
|
80 |
in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end |
54526 | 81 |
|
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
82 |
fun resolve_files keywords master_dir (blobs, blobs_index) toks = |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57844
diff
changeset
|
83 |
(case Outer_Syntax.parse_spans toks of |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
84 |
[Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] => |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
85 |
(case try (nth toks) blobs_index of |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
86 |
SOME tok => |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
87 |
let |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
88 |
val pos = Token.pos_of tok; |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
89 |
val path = Path.explode (Token.content_of tok) |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
90 |
handle ERROR msg => error (msg ^ Position.here pos); |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
91 |
fun make_file src_path (Exn.Res (file_node, NONE)) = |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
92 |
Exn.interruptible_capture (fn () => |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
93 |
read_file_node file_node master_dir pos src_path) () |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
94 |
| make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = |
60027
c42d65e11b6e
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
wenzelm
parents:
59944
diff
changeset
|
95 |
(Position.report pos Markup.language_path; |
c42d65e11b6e
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
wenzelm
parents:
59944
diff
changeset
|
96 |
Exn.Res (blob_file src_path lines digest file_node)) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
97 |
| make_file _ (Exn.Exn e) = Exn.Exn e; |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
98 |
val src_paths = Keyword.command_files keywords cmd path; |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
99 |
val files = |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
100 |
if null blobs then |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
101 |
map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
102 |
else if length src_paths = length blobs then |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
103 |
map2 make_file src_paths blobs |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
104 |
else error ("Misalignment of inlined files" ^ Position.here pos); |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
105 |
in |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
106 |
toks |> map_index (fn (i, tok) => |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
107 |
if i = blobs_index then Token.put_files files tok else tok) |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
108 |
end |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
109 |
| NONE => toks) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
110 |
| _ => toks); |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53976
diff
changeset
|
111 |
|
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
112 |
fun reports_of_token keywords tok = |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
113 |
let |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
114 |
val malformed_symbols = |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
115 |
Input.source_explode (Token.input_of tok) |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
116 |
|> map_filter (fn (sym, pos) => |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
117 |
if Symbol.is_malformed sym |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
118 |
then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE); |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
119 |
val is_malformed = Token.is_error tok orelse not (null malformed_symbols); |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
120 |
val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols; |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
121 |
in (is_malformed, reports) end; |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
122 |
|
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
|
123 |
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
|
124 |
|
60095 | 125 |
fun read_thy st = Toplevel.theory_of st |
126 |
handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy; |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
127 |
|
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
128 |
fun read keywords thy master_dir init blobs_info span = |
52510 | 129 |
let |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
130 |
val command_reports = Outer_Syntax.command_reports thy; |
52509 | 131 |
|
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
132 |
val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span)); |
52510 | 133 |
val pos = |
134 |
(case find_first Token.is_command span of |
|
55708 | 135 |
SOME tok => Token.pos_of tok |
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
136 |
| NONE => #1 proper_range); |
52509 | 137 |
|
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
138 |
val token_reports = map (reports_of_token keywords) span; |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
139 |
val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span); |
52510 | 140 |
in |
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61213
diff
changeset
|
141 |
if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax" |
52510 | 142 |
else |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
143 |
(case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of |
58853 | 144 |
[tr] => Toplevel.modify_init init tr |
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
145 |
| [] => Toplevel.ignored (#1 (Token.range_of span)) |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
146 |
| _ => 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
|
147 |
handle ERROR msg => Toplevel.malformed (#1 proper_range) msg |
52510 | 148 |
end; |
52509 | 149 |
|
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
|
150 |
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
|
151 |
|
52509 | 152 |
|
153 |
(* eval *) |
|
47336 | 154 |
|
59472
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
155 |
type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state}; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
156 |
val init_eval_state = {failed = false, command = Toplevel.empty, state = Toplevel.toplevel}; |
52600 | 157 |
|
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
158 |
datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy}; |
52600 | 159 |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
160 |
fun eval_exec_id (Eval {exec_id, ...}) = exec_id; |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58934
diff
changeset
|
161 |
val eval_eq = op = o apply2 eval_exec_id; |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
162 |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
163 |
val eval_running = Execution.is_running_exec o eval_exec_id; |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
164 |
fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process; |
52772 | 165 |
|
59466
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
166 |
fun eval_result (Eval {eval_process, ...}) = |
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
167 |
task_context (Future.worker_subgroup ()) Lazy.force eval_process; |
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
168 |
|
52600 | 169 |
val eval_result_state = #state o eval_result; |
170 |
||
47336 | 171 |
local |
172 |
||
58923 | 173 |
fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () => |
56937 | 174 |
let |
175 |
val name = Toplevel.name_of tr; |
|
176 |
val res = |
|
58923 | 177 |
if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0 |
178 |
else if Keyword.is_proof keywords name then Toplevel.reset_proof st0 |
|
56937 | 179 |
else NONE; |
180 |
in |
|
181 |
(case res of |
|
182 |
NONE => st0 |
|
60076 | 183 |
| SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st)) |
56937 | 184 |
end) (); |
185 |
||
58923 | 186 |
fun run keywords int tr st = |
187 |
if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then |
|
53192 | 188 |
(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
|
189 |
(fn () => Toplevel.command_exception int tr st); ([], SOME st)) |
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51266
diff
changeset
|
190 |
else Toplevel.command_errors int tr st; |
47336 | 191 |
|
52510 | 192 |
fun check_cmts span tr st' = |
193 |
Toplevel.setmp_thread_position tr |
|
194 |
(fn () => |
|
195 |
Outer_Syntax.side_comments span |> maps (fn cmt => |
|
59809 | 196 |
(Thy_Output.check_text (Token.input_of cmt) st'; []) |
52619
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
197 |
handle exn => |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
198 |
if Exn.is_interrupt exn then reraise exn |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56292
diff
changeset
|
199 |
else Runtime.exn_messages_ids exn)) (); |
52510 | 200 |
|
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
|
201 |
fun report tr m = |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56303
diff
changeset
|
202 |
Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) (); |
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
|
203 |
|
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 |
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
|
205 |
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
|
206 |
|
47336 | 207 |
fun proof_status tr st = |
208 |
(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
|
209 |
SOME prf => status tr (Proof.status_markup prf) |
47336 | 210 |
| NONE => ()); |
211 |
||
59472
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
212 |
fun eval_state keywords span tr ({state, ...}: eval_state) = |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
213 |
let |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
214 |
val _ = Multithreading.interrupted (); |
47336 | 215 |
|
59472
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
216 |
val st = reset_state keywords tr state; |
56937 | 217 |
|
59472
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
218 |
val _ = status tr Markup.running; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
219 |
val (errs1, result) = run keywords true tr st; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
220 |
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
221 |
val errs = errs1 @ errs2; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
222 |
val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
223 |
in |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
224 |
(case result of |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
225 |
NONE => |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
226 |
let |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
227 |
val _ = status tr Markup.failed; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
228 |
val _ = status tr Markup.finished; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
229 |
val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else (); |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
230 |
in {failed = true, command = tr, state = st} end |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
231 |
| SOME st' => |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
232 |
let |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
233 |
val _ = proof_status tr st'; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
234 |
val _ = status tr Markup.finished; |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
235 |
in {failed = false, command = tr, state = st'} end) |
513300fa2d09
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents:
59466
diff
changeset
|
236 |
end; |
47336 | 237 |
|
52534 | 238 |
in |
239 |
||
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
240 |
fun eval keywords master_dir init blobs_info span eval0 = |
52534 | 241 |
let |
242 |
val exec_id = Document_ID.make (); |
|
243 |
fun process () = |
|
244 |
let |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
245 |
val eval_state0 = eval_result eval0; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
246 |
val thy = read_thy (#state eval_state0); |
52534 | 247 |
val tr = |
248 |
Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) |
|
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
249 |
(fn () => |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59685
diff
changeset
|
250 |
read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) (); |
58934
385a4cc7426f
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
wenzelm
parents:
58928
diff
changeset
|
251 |
in eval_state keywords span tr eval_state0 end; |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
252 |
in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end; |
52534 | 253 |
|
47336 | 254 |
end; |
255 |
||
52509 | 256 |
|
257 |
(* print *) |
|
258 |
||
52600 | 259 |
datatype print = Print of |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
260 |
{name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
261 |
exec_id: Document_ID.exec, print_process: unit lazy}; |
52600 | 262 |
|
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
263 |
fun print_exec_id (Print {exec_id, ...}) = exec_id; |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58934
diff
changeset
|
264 |
val print_eq = op = o apply2 print_exec_id; |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
265 |
|
52526 | 266 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit; |
52515 | 267 |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
268 |
type print_function = |
58923 | 269 |
{keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> |
52953
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52853
diff
changeset
|
270 |
{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
|
271 |
|
52511 | 272 |
local |
273 |
||
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
274 |
val print_functions = |
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
275 |
Synchronized.var "Command.print_functions" ([]: (string * print_function) list); |
52511 | 276 |
|
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
56034
diff
changeset
|
277 |
fun print_error tr opt_context e = |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56292
diff
changeset
|
278 |
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () |
52619
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
279 |
handle exn => |
70d5f2f7d27f
reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents:
52609
diff
changeset
|
280 |
if Exn.is_interrupt exn then reraise exn |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56303
diff
changeset
|
281 |
else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn); |
52516
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
282 |
|
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
283 |
fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process; |
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
284 |
|
52600 | 285 |
fun print_persistent (Print {persistent, ...}) = persistent; |
52596
40298d383463
global management of command execution fragments;
wenzelm
parents:
52586
diff
changeset
|
286 |
|
52853
4ab66773a41f
prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents:
52850
diff
changeset
|
287 |
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
|
288 |
|
52511 | 289 |
in |
52509 | 290 |
|
58923 | 291 |
fun print command_visible command_overlays keywords command_name eval old_prints = |
52570 | 292 |
let |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
293 |
val print_functions = Synchronized.value print_functions; |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
294 |
|
52999
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
295 |
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
|
296 |
let |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
297 |
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
|
298 |
fun process () = |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
299 |
let |
1f09c98a3232
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents:
52953
diff
changeset
|
300 |
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
|
301 |
val tr = Toplevel.exec_id exec_id command; |
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
56034
diff
changeset
|
302 |
val opt_context = try Toplevel.generic_theory_of st'; |
52999
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 () |
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
56034
diff
changeset
|
305 |
else print_error tr opt_context (fn () => print_fn tr st') |
52999
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, |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
310 |
exec_id = exec_id, print_process = Lazy.lazy process} |
52999
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 |
58923 | 319 |
val params = |
320 |
{keywords = keywords, |
|
321 |
command_name = command_name, |
|
322 |
args = args, |
|
323 |
exec_id = eval_exec_id eval}; |
|
52570 | 324 |
in |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56292
diff
changeset
|
325 |
(case Exn.capture (Runtime.controlled_execution NONE get_pr) params of |
52570 | 326 |
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
|
327 |
| 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
|
328 |
| Exn.Exn exn => SOME (bad_print name args exn)) |
52570 | 329 |
end; |
330 |
||
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
331 |
fun get_print (a, b) = |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
332 |
(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
|
333 |
NONE => |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
334 |
(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
|
335 |
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
|
336 |
| 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
|
337 |
| some => some); |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
338 |
|
52570 | 339 |
val new_prints = |
340 |
if command_visible then |
|
52853
4ab66773a41f
prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents:
52850
diff
changeset
|
341 |
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
|
342 |
|> sort_distinct overlay_ord |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52785
diff
changeset
|
343 |
|> map_filter get_print |
52656
9437f440ef3f
keep persistent prints only if actually finished;
wenzelm
parents:
52651
diff
changeset
|
344 |
else filter (fn print => print_finished print andalso print_persistent print) old_prints; |
52570 | 345 |
in |
52600 | 346 |
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints |
52570 | 347 |
end; |
52511 | 348 |
|
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
349 |
fun print_function name f = |
52511 | 350 |
Synchronized.change print_functions (fn funs => |
351 |
(if not (AList.defined (op =) funs name) then () |
|
352 |
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
|
353 |
AList.update (op =) (name, f) funs)); |
52511 | 354 |
|
52571 | 355 |
fun no_print_function name = |
356 |
Synchronized.change print_functions (filter_out (equal name o #1)); |
|
357 |
||
52511 | 358 |
end; |
359 |
||
52526 | 360 |
val _ = |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
361 |
print_function "Execution.print" |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
362 |
(fn {args, exec_id, ...} => |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
363 |
if null args then |
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60095
diff
changeset
|
364 |
SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false, |
56292 | 365 |
print_fn = fn _ => fn _ => Execution.fork_prints exec_id} |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
366 |
else NONE); |
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
367 |
|
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
368 |
val _ = |
52647
45ce95b8bf69
determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents:
52619
diff
changeset
|
369 |
print_function "print_state" |
58923 | 370 |
(fn {keywords, command_name, ...} => |
61213 | 371 |
if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name |
372 |
then |
|
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60095
diff
changeset
|
373 |
SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false, |
61208 | 374 |
print_fn = fn _ => fn st => |
375 |
if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st) |
|
376 |
else ()} |
|
56895
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56887
diff
changeset
|
377 |
else NONE); |
52509 | 378 |
|
52532 | 379 |
|
52600 | 380 |
(* combined execution *) |
381 |
||
382 |
type exec = eval * print list; |
|
383 |
val no_exec: exec = |
|
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
384 |
(Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []); |
52532 | 385 |
|
52600 | 386 |
fun exec_ids NONE = [] |
56291
e79f76a48449
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents:
56265
diff
changeset
|
387 |
| exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; |
52600 | 388 |
|
389 |
local |
|
390 |
||
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
391 |
fun run_process execution_id exec_id process = |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
392 |
let val group = Future.worker_subgroup () in |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
393 |
if Execution.running execution_id exec_id [group] then |
59466
6fab87db556c
ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents:
59348
diff
changeset
|
394 |
ignore (task_context group Lazy.force_result process) |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
395 |
else () |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
396 |
end; |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
397 |
|
59328
b83d6c3c439a
ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents:
59193
diff
changeset
|
398 |
fun ignore_process process = |
b83d6c3c439a
ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents:
59193
diff
changeset
|
399 |
Lazy.is_running process orelse Lazy.is_finished process; |
b83d6c3c439a
ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents:
59193
diff
changeset
|
400 |
|
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
401 |
fun run_eval execution_id (Eval {exec_id, eval_process}) = |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
402 |
if Lazy.is_finished eval_process then () |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
403 |
else run_process execution_id exec_id eval_process; |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
404 |
|
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
405 |
fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) = |
59328
b83d6c3c439a
ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents:
59193
diff
changeset
|
406 |
if ignore_process print_process then () |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
407 |
else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print") |
56875
f6259d6fb565
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
wenzelm
parents:
56504
diff
changeset
|
408 |
then |
52651 | 409 |
let |
410 |
val group = Future.worker_subgroup (); |
|
411 |
fun fork () = |
|
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
412 |
ignore ((singleton o Future.forks) |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
413 |
{name = name, group = SOME group, deps = [], pri = pri, interrupts = true} |
59328
b83d6c3c439a
ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents:
59193
diff
changeset
|
414 |
(fn () => |
b83d6c3c439a
ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents:
59193
diff
changeset
|
415 |
if ignore_process print_process then () |
b83d6c3c439a
ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents:
59193
diff
changeset
|
416 |
else run_process execution_id exec_id print_process)); |
52651 | 417 |
in |
52762 | 418 |
(case delay of |
419 |
NONE => fork () |
|
420 |
| SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork)) |
|
52651 | 421 |
end |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
422 |
else run_process execution_id exec_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
|
423 |
|
52600 | 424 |
in |
425 |
||
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
426 |
fun exec execution_id (eval, prints) = |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59188
diff
changeset
|
427 |
(run_eval execution_id eval; List.app (run_print execution_id) prints); |
52532 | 428 |
|
47336 | 429 |
end; |
430 |
||
52600 | 431 |
end; |
432 |