author | wenzelm |
Mon, 10 Aug 2015 20:22:49 +0200 | |
changeset 60880 | fa958e24ff24 |
parent 60198 | 8483c2883c8c |
child 60937 | 51425cbe8ce9 |
permissions | -rw-r--r-- |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/PIDE/document.ML |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
3 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
4 |
Document as collection of named nodes, each consisting of an editable |
52536 | 5 |
list of commands, associated with asynchronous execution process. |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
6 |
*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
7 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
8 |
signature DOCUMENT = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
9 |
sig |
52796 | 10 |
val timing: bool Unsynchronized.ref |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
11 |
type node_header = {master: string, header: Thy_Header.header, errors: string list} |
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52850
diff
changeset
|
12 |
type overlay = Document_ID.command * (string * string list) |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
13 |
datatype node_edit = |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
14 |
Edits of (Document_ID.command option * Document_ID.command option) list | |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47633
diff
changeset
|
15 |
Deps of node_header | |
52849 | 16 |
Perspective of bool * Document_ID.command list * overlay list |
44156 | 17 |
type edit = string * node_edit |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
18 |
type state |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
19 |
val init_state: state |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
20 |
val define_blob: string -> string -> state -> state |
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
21 |
type blob_digest = (string * string option) Exn.result |
59685
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
22 |
val define_command: Document_ID.command -> string -> blob_digest list -> int -> |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset
|
23 |
((int * int) * string) list -> state -> state |
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60198
diff
changeset
|
24 |
val command_exec: state -> string -> Document_ID.command -> Command.exec option |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
25 |
val remove_versions: Document_ID.version list -> state -> state |
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
26 |
val start_execution: state -> state |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
27 |
val update: Document_ID.version -> Document_ID.version -> edit list -> state -> |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
28 |
Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state |
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
29 |
val state: unit -> state |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
30 |
val change_state: (state -> state) -> unit |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
31 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
32 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
33 |
structure Document: DOCUMENT = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
34 |
struct |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
35 |
|
52796 | 36 |
val timing = Unsynchronized.ref false; |
37 |
fun timeit msg e = cond_timeit (! timing) msg e; |
|
38 |
||
39 |
||
40 |
||
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
41 |
(** document structure **) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
42 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
43 |
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id); |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
44 |
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id); |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
45 |
|
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
46 |
type node_header = |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
47 |
{master: string, header: Thy_Header.header, errors: string list}; |
52849 | 48 |
|
49 |
type perspective = |
|
50 |
{required: bool, (*required node*) |
|
51 |
visible: Inttab.set, (*visible commands*) |
|
52 |
visible_last: Document_ID.command option, (*last visible command*) |
|
57874 | 53 |
overlays: (string * string list) list Inttab.table}; (*command id -> print functions with args*) |
52849 | 54 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
55 |
structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord); |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
56 |
|
43668 | 57 |
abstype node = Node of |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47633
diff
changeset
|
58 |
{header: node_header, (*master directory, theory header, errors*) |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
59 |
keywords: Keyword.keywords option, (*outer syntax keywords*) |
52849 | 60 |
perspective: perspective, (*command perspective*) |
52761
909167fdd367
discontinued notion of "stable" result -- running execution is never canceled;
wenzelm
parents:
52716
diff
changeset
|
61 |
entries: Command.exec option Entries.T, (*command entries with excecutions*) |
52526 | 62 |
result: Command.eval option} (*result of last execution*) |
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
63 |
and version = Version of node String_Graph.T (*development graph wrt. static imports*) |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
64 |
with |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
65 |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
66 |
fun make_node (header, keywords, perspective, entries, result) = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
67 |
Node {header = header, keywords = keywords, perspective = perspective, |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
68 |
entries = entries, result = result}; |
43668 | 69 |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
70 |
fun map_node f (Node {header, keywords, perspective, entries, result}) = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
71 |
make_node (f (header, keywords, perspective, entries, result)); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
72 |
|
52849 | 73 |
fun make_perspective (required, command_ids, overlays) : perspective = |
74 |
{required = required, |
|
75 |
visible = Inttab.make_set command_ids, |
|
76 |
visible_last = try List.last command_ids, |
|
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52850
diff
changeset
|
77 |
overlays = Inttab.make_list overlays}; |
44441 | 78 |
|
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
79 |
val no_header: node_header = |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
80 |
{master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []}; |
52849 | 81 |
val no_perspective = make_perspective (false, [], []); |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset
|
82 |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
83 |
val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE); |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset
|
84 |
|
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
85 |
fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) = |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
86 |
not required andalso |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
87 |
Inttab.is_empty visible andalso |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
88 |
is_none visible_last andalso |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
89 |
Inttab.is_empty overlays; |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
90 |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
91 |
fun is_empty_node (Node {header, keywords, perspective, entries, result}) = |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
92 |
header = no_header andalso |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
93 |
is_none keywords andalso |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
94 |
is_no_perspective perspective andalso |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
95 |
Entries.is_empty entries andalso |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
96 |
is_none result; |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56801
diff
changeset
|
97 |
|
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset
|
98 |
|
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset
|
99 |
(* basic components *) |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset
|
100 |
|
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
101 |
fun master_directory (Node {header = {master, ...}, ...}) = |
54558
31844ca390ad
more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
wenzelm
parents:
54526
diff
changeset
|
102 |
(case try Url.explode master of |
31844ca390ad
more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
wenzelm
parents:
54526
diff
changeset
|
103 |
SOME (Url.File path) => path |
31844ca390ad
more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
wenzelm
parents:
54526
diff
changeset
|
104 |
| _ => Path.current); |
31844ca390ad
more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
wenzelm
parents:
54526
diff
changeset
|
105 |
|
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
106 |
fun set_header master header errors = |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
107 |
map_node (fn (_, keywords, perspective, entries, result) => |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
108 |
({master = master, header = header, errors = errors}, keywords, perspective, entries, result)); |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
109 |
|
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
110 |
fun get_header (Node {header, ...}) = header; |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47633
diff
changeset
|
111 |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
112 |
fun set_keywords keywords = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
113 |
map_node (fn (header, _, perspective, entries, result) => |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
114 |
(header, keywords, perspective, entries, result)); |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
115 |
|
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
116 |
fun get_keywords (Node {keywords, ...}) = keywords; |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
117 |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset
|
118 |
fun read_header node span = |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset
|
119 |
let |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
120 |
val {header, errors, ...} = get_header node; |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
121 |
val _ = |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
122 |
if null errors then () |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
123 |
else |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
124 |
cat_lines errors |> |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
125 |
(case Position.get_id (Position.thread_data ()) of |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
126 |
NONE => I |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
127 |
| SOME id => Protocol_Message.command_positions_yxml id) |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
128 |
|> error; |
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
129 |
val {name = (name, _), imports, ...} = header; |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
130 |
val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span; |
54526 | 131 |
in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end; |
132 |
||
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
133 |
fun get_perspective (Node {perspective, ...}) = perspective; |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
134 |
|
52808
143f225e50f5
allow explicit indication of required node: full eval, no prints;
wenzelm
parents:
52798
diff
changeset
|
135 |
fun set_perspective args = |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
136 |
map_node (fn (header, keywords, _, entries, result) => |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
137 |
(header, keywords, make_perspective args, entries, result)); |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
138 |
|
52849 | 139 |
val required_node = #required o get_perspective; |
140 |
val visible_command = Inttab.defined o #visible o get_perspective; |
|
141 |
val visible_last = #visible_last o get_perspective; |
|
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset
|
142 |
val visible_node = is_some o visible_last |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52849
diff
changeset
|
143 |
val overlays = Inttab.lookup_list o #overlays o get_perspective; |
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset
|
144 |
|
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset
|
145 |
fun map_entries f = |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
146 |
map_node (fn (header, keywords, perspective, entries, result) => |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
147 |
(header, keywords, perspective, f entries, result)); |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
148 |
|
52761
909167fdd367
discontinued notion of "stable" result -- running execution is never canceled;
wenzelm
parents:
52716
diff
changeset
|
149 |
fun get_entries (Node {entries, ...}) = entries; |
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
150 |
|
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
151 |
fun iterate_entries f = Entries.iterate NONE f o get_entries; |
52761
909167fdd367
discontinued notion of "stable" result -- running execution is never canceled;
wenzelm
parents:
52716
diff
changeset
|
152 |
fun iterate_entries_after start f (Node {entries, ...}) = |
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
153 |
(case Entries.get_after entries start of |
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
154 |
NONE => I |
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
155 |
| SOME id => Entries.iterate (SOME id) f entries); |
43668 | 156 |
|
47339
79bd24497ffd
tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
wenzelm
parents:
47336
diff
changeset
|
157 |
fun get_result (Node {result, ...}) = result; |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
158 |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
159 |
fun set_result result = |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
160 |
map_node (fn (header, keywords, perspective, entries, _) => |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
161 |
(header, keywords, perspective, entries, result)); |
44180 | 162 |
|
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
163 |
fun changed_result node node' = |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
164 |
(case (get_result node, get_result node') of |
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52606
diff
changeset
|
165 |
(SOME eval, SOME eval') => not (Command.eval_eq (eval, eval')) |
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
166 |
| (NONE, NONE) => false |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
167 |
| _ => true); |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
168 |
|
52772 | 169 |
fun pending_result node = |
170 |
(case get_result node of |
|
171 |
SOME eval => not (Command.eval_finished eval) |
|
172 |
| NONE => false); |
|
52533 | 173 |
|
59198
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
174 |
fun finished_result node = |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
175 |
(case get_result node of |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
176 |
SOME eval => Command.eval_finished eval |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
177 |
| NONE => false); |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
178 |
|
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
179 |
fun loaded_theory name = |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
180 |
(case try (unsuffix ".thy") name of |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
181 |
SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a] |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
182 |
| NONE => NONE); |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
183 |
|
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
184 |
fun get_node nodes name = String_Graph.get_node nodes name |
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
185 |
handle String_Graph.UNDEF _ => empty_node; |
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
186 |
fun default_node name = String_Graph.default_node (name, empty_node); |
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
187 |
fun update_node name f = default_node name #> String_Graph.map_node name f; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
188 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
189 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
190 |
(* node edits and associated executions *) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
191 |
|
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52850
diff
changeset
|
192 |
type overlay = Document_ID.command * (string * string list); |
52849 | 193 |
|
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
194 |
datatype node_edit = |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
195 |
Edits of (Document_ID.command option * Document_ID.command option) list | |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47633
diff
changeset
|
196 |
Deps of node_header | |
52849 | 197 |
Perspective of bool * Document_ID.command list * overlay list; |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
198 |
|
44156 | 199 |
type edit = string * node_edit; |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
200 |
|
49064
bd6cc0b911a1
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset
|
201 |
val after_entry = Entries.get_after o get_entries; |
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset
|
202 |
|
49064
bd6cc0b911a1
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset
|
203 |
fun lookup_entry node id = |
bd6cc0b911a1
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset
|
204 |
(case Entries.lookup (get_entries node) id of |
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset
|
205 |
NONE => NONE |
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset
|
206 |
| SOME (exec, _) => exec); |
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset
|
207 |
|
49064
bd6cc0b911a1
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset
|
208 |
fun the_entry node id = |
bd6cc0b911a1
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset
|
209 |
(case Entries.lookup (get_entries node) id of |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
210 |
NONE => err_undef "command entry" id |
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset
|
211 |
| SOME (exec, _) => exec); |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
212 |
|
52532 | 213 |
fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id)) |
214 |
| the_default_entry _ NONE = (Document_ID.none, Command.no_exec); |
|
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset
|
215 |
|
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
216 |
fun assign_entry (command_id, exec) node = |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
217 |
if is_none (Entries.lookup (get_entries node) command_id) then node |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
218 |
else map_entries (Entries.update (command_id, exec)) node; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
219 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
220 |
fun reset_after id entries = |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
221 |
(case Entries.get_after entries id of |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
222 |
NONE => entries |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
223 |
| SOME next => Entries.update (next, NONE) entries); |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
224 |
|
43668 | 225 |
val edit_node = map_entries o fold |
226 |
(fn (id, SOME id2) => Entries.insert_after id (id2, NONE) |
|
227 |
| (id, NONE) => Entries.delete_after id #> reset_after id); |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
228 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
229 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
230 |
(* version operations *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
231 |
|
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
232 |
val empty_version = Version String_Graph.empty; |
44185 | 233 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
234 |
fun nodes_of (Version nodes) = nodes; |
44185 | 235 |
val node_of = get_node o nodes_of; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
236 |
|
44185 | 237 |
fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); |
44180 | 238 |
|
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
239 |
fun edit_nodes (name, node_edit) (Version nodes) = |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
240 |
Version |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset
|
241 |
(case node_edit of |
54562
301a721af68b
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
wenzelm
parents:
54558
diff
changeset
|
242 |
Edits edits => update_node name (edit_node edits) nodes |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
243 |
| Deps {master, header, errors} => |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset
|
244 |
let |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset
|
245 |
val imports = map fst (#imports header); |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset
|
246 |
val nodes1 = nodes |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset
|
247 |
|> default_node name |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset
|
248 |
|> fold default_node imports; |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset
|
249 |
val nodes2 = nodes1 |
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
250 |
|> String_Graph.Keys.fold |
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
251 |
(fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name); |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
252 |
val (nodes3, errors1) = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
253 |
(String_Graph.add_deps_acyclic (name, imports) nodes2, errors) |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
254 |
handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs); |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
255 |
in String_Graph.map_node name (set_header master header errors1) nodes3 end |
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset
|
256 |
| Perspective perspective => update_node name (set_perspective perspective) nodes); |
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset
|
257 |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
258 |
fun update_keywords name nodes = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
259 |
nodes |> String_Graph.map_node name (fn node => |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
260 |
if is_empty_node node then node |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
261 |
else |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
262 |
let |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
263 |
val {master, header, errors} = get_header node; |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
264 |
val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header); |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
265 |
val keywords = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
266 |
Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords); |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
267 |
val (keywords', errors') = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
268 |
(Keyword.add_keywords (#keywords header) keywords, errors) |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
269 |
handle ERROR msg => |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
270 |
(keywords, if member (op =) errors msg then errors else errors @ [msg]); |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
271 |
in |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
272 |
node |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
273 |
|> set_header master header errors' |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
274 |
|> set_keywords (SOME keywords') |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
275 |
end); |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
276 |
|
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
277 |
fun edit_keywords edits (Version nodes) = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
278 |
Version |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
279 |
(fold update_keywords |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
280 |
(String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits)) |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
281 |
nodes); |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
282 |
|
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset
|
283 |
fun put_node (name, node) (Version nodes) = |
57616 | 284 |
let |
285 |
val nodes1 = update_node name (K node) nodes; |
|
286 |
val nodes2 = |
|
287 |
if String_Graph.is_maximal nodes1 name andalso is_empty_node node |
|
288 |
then String_Graph.del_node name nodes1 |
|
289 |
else nodes1; |
|
290 |
in Version nodes2 end; |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
291 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
292 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
293 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
294 |
|
52595 | 295 |
|
296 |
(** main state -- document structure and execution process **) |
|
52536 | 297 |
|
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
298 |
type blob_digest = (string * string option) Exn.result; (*file node name, raw digest*) |
55798 | 299 |
|
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
300 |
type execution = |
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
301 |
{version_id: Document_ID.version, (*static version id*) |
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
302 |
execution_id: Document_ID.execution, (*dynamic execution 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:
59086
diff
changeset
|
303 |
delay_request: unit future}; (*pending event timer request*) |
52604 | 304 |
|
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
305 |
val no_execution: execution = |
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:
59086
diff
changeset
|
306 |
{version_id = Document_ID.none, |
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:
59086
diff
changeset
|
307 |
execution_id = Document_ID.none, |
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:
59086
diff
changeset
|
308 |
delay_request = Future.value ()}; |
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
309 |
|
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:
59086
diff
changeset
|
310 |
fun new_execution version_id delay_request : execution = |
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:
59086
diff
changeset
|
311 |
{version_id = version_id, |
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:
59086
diff
changeset
|
312 |
execution_id = Execution.start (), |
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:
59086
diff
changeset
|
313 |
delay_request = delay_request}; |
52604 | 314 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
315 |
abstype state = State of |
52536 | 316 |
{versions: version Inttab.table, (*version id -> document content*) |
55798 | 317 |
blobs: (SHA1.digest * string list) Symtab.table, (*raw digest -> digest, lines*) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59687
diff
changeset
|
318 |
commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table, |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59687
diff
changeset
|
319 |
(*command id -> name, inlined files, token index of files, command span*) |
52536 | 320 |
execution: execution} (*current execution process*) |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
321 |
with |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
322 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
323 |
fun make_state (versions, blobs, commands, execution) = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
324 |
State {versions = versions, blobs = blobs, commands = commands, execution = execution}; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
325 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
326 |
fun map_state f (State {versions, blobs, commands, execution}) = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
327 |
make_state (f (versions, blobs, commands, execution)); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
328 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
329 |
val init_state = |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
330 |
make_state (Inttab.make [(Document_ID.none, empty_version)], |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
331 |
Symtab.empty, Inttab.empty, no_execution); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
332 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
333 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
334 |
(* document versions *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
335 |
|
52536 | 336 |
fun define_version version_id version = |
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:
59086
diff
changeset
|
337 |
map_state (fn (versions, blobs, commands, {delay_request, ...}) => |
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
338 |
let |
52536 | 339 |
val versions' = Inttab.update_new (version_id, version) versions |
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
340 |
handle Inttab.DUP dup => err_dup "document version" dup; |
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:
59086
diff
changeset
|
341 |
val execution' = new_execution version_id delay_request; |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
342 |
in (versions', blobs, commands, execution') end); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
343 |
|
52536 | 344 |
fun the_version (State {versions, ...}) version_id = |
345 |
(case Inttab.lookup versions version_id of |
|
346 |
NONE => err_undef "document version" version_id |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
347 |
| SOME version => version); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
348 |
|
52536 | 349 |
fun delete_version version_id versions = |
350 |
Inttab.delete version_id versions |
|
351 |
handle Inttab.UNDEF _ => err_undef "document version" version_id; |
|
44673 | 352 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
353 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
354 |
(* inlined files *) |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
355 |
|
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
356 |
fun define_blob digest text = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
357 |
map_state (fn (versions, blobs, commands, execution) => |
57638
ed58e740a699
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents:
57616
diff
changeset
|
358 |
let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
359 |
in (versions, blobs', commands, execution) end); |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
360 |
|
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
361 |
fun the_blob (State {blobs, ...}) digest = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
362 |
(case Symtab.lookup blobs digest of |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
363 |
NONE => error ("Undefined blob: " ^ digest) |
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:
54562
diff
changeset
|
364 |
| SOME content => content); |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
365 |
|
56447
1e77ed11f2f7
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents:
56208
diff
changeset
|
366 |
fun resolve_blob state (blob_digest: blob_digest) = |
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
367 |
blob_digest |> Exn.map_result (fn (file_node, raw_digest) => |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
368 |
(file_node, Option.map (the_blob state) raw_digest)); |
56447
1e77ed11f2f7
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents:
56208
diff
changeset
|
369 |
|
59685
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
370 |
fun blob_reports pos (blob_digest: blob_digest) = |
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
371 |
(case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []); |
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
372 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
373 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
374 |
(* commands *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
375 |
|
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59689
diff
changeset
|
376 |
fun define_command command_id name blobs_digests blobs_index toks = |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
377 |
map_state (fn (versions, blobs, commands, execution) => |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
378 |
let |
52536 | 379 |
val id = Document_ID.print command_id; |
380 |
val span = |
|
381 |
Lazy.lazy (fn () => |
|
382 |
Position.setmp_thread_data (Position.id_only id) |
|
59685
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
383 |
(fn () => |
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
384 |
let |
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
385 |
val (tokens, _) = fold_map Token.make toks (Position.id id); |
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
386 |
val _ = |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59689
diff
changeset
|
387 |
if blobs_index < 0 |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59689
diff
changeset
|
388 |
then (*inlined errors*) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59689
diff
changeset
|
389 |
map_filter Exn.get_exn blobs_digests |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59689
diff
changeset
|
390 |
|> List.app (Output.error_message o Runtime.exn_message) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59689
diff
changeset
|
391 |
else (*auxiliary files*) |
60027
c42d65e11b6e
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
wenzelm
parents:
59934
diff
changeset
|
392 |
let val pos = Token.pos_of (nth tokens blobs_index) |
c42d65e11b6e
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
wenzelm
parents:
59934
diff
changeset
|
393 |
in Position.reports (maps (blob_reports pos) blobs_digests) end; |
59685
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
394 |
in tokens end) ()); |
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
395 |
val commands' = |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59689
diff
changeset
|
396 |
Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands |
59685
c043306d2598
clarified markup for embedded files, early before execution;
wenzelm
parents:
59347
diff
changeset
|
397 |
handle Inttab.DUP dup => err_dup "command" dup; |
47395
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset
|
398 |
val _ = |
52536 | 399 |
Position.setmp_thread_data (Position.id_only id) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49906
diff
changeset
|
400 |
(fn () => Output.status (Markup.markup_only Markup.accepted)) (); |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
401 |
in (versions, blobs, commands', execution) end); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
402 |
|
52536 | 403 |
fun the_command (State {commands, ...}) command_id = |
404 |
(case Inttab.lookup commands command_id of |
|
405 |
NONE => err_undef "command" command_id |
|
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44643
diff
changeset
|
406 |
| SOME command => command); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
407 |
|
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
408 |
val the_command_name = #1 oo the_command; |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
409 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60198
diff
changeset
|
410 |
fun command_exec state node_name command_id = |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60198
diff
changeset
|
411 |
let |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60198
diff
changeset
|
412 |
val State {execution = {version_id, ...}, ...} = state; |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60198
diff
changeset
|
413 |
val node = get_node (nodes_of (the_version state version_id)) node_name; |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60198
diff
changeset
|
414 |
in the_entry node command_id end; |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60198
diff
changeset
|
415 |
|
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
416 |
end; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
417 |
|
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
418 |
|
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
419 |
(* remove_versions *) |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
420 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
421 |
fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) => |
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
422 |
let |
52536 | 423 |
val _ = |
424 |
member (op =) version_ids (#version_id execution) andalso |
|
425 |
error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution)); |
|
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
47342
diff
changeset
|
426 |
|
52536 | 427 |
val versions' = fold delete_version version_ids versions; |
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
428 |
val commands' = |
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
429 |
(versions', Inttab.empty) |-> |
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
430 |
Inttab.fold (fn (_, version) => nodes_of version |> |
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
431 |
String_Graph.fold (fn (_, (node, _)) => node |> |
52536 | 432 |
iterate_entries (fn ((_, command_id), _) => |
433 |
SOME o Inttab.insert (K true) (command_id, the_command state command_id)))); |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
434 |
val blobs' = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
435 |
(commands', Symtab.empty) |-> |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59687
diff
changeset
|
436 |
Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |> |
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
437 |
fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I)); |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
438 |
|
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
439 |
in (versions', blobs', commands', execution) end); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
440 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
441 |
|
52604 | 442 |
(* document execution *) |
47389
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset
|
443 |
|
60198
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
444 |
fun make_required nodes = |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
445 |
let |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
446 |
fun all_preds P = |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
447 |
String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes [] |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
448 |
|> String_Graph.all_preds nodes |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
449 |
|> Symtab.make_set; |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
450 |
|
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
451 |
val all_visible = all_preds visible_node; |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
452 |
val all_required = all_preds required_node; |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
453 |
in |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
454 |
Symtab.fold (fn (a, ()) => |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
455 |
exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
456 |
Symtab.update (a, ())) all_visible all_required |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
457 |
end; |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
458 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
459 |
fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) => |
52796 | 460 |
timeit "Document.start_execution" (fn () => |
461 |
let |
|
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:
59086
diff
changeset
|
462 |
val {version_id, execution_id, delay_request} = execution; |
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52797
diff
changeset
|
463 |
|
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52797
diff
changeset
|
464 |
val delay = seconds (Options.default_real "editor_execution_delay"); |
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
465 |
|
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52797
diff
changeset
|
466 |
val _ = Future.cancel delay_request; |
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52797
diff
changeset
|
467 |
val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay)); |
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52797
diff
changeset
|
468 |
|
59198
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
469 |
fun finished_import (name, (node, _)) = |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
470 |
finished_result node orelse is_some (loaded_theory name); |
60198
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
471 |
|
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
472 |
val nodes = nodes_of (the_version state version_id); |
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
473 |
val required = make_required nodes; |
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:
59086
diff
changeset
|
474 |
val _ = |
60198
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
475 |
nodes |> String_Graph.schedule |
52573
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset
|
476 |
(fn deps => fn (name, node) => |
60198
8483c2883c8c
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
wenzelm
parents:
60027
diff
changeset
|
477 |
if Symtab.defined required name orelse visible_node node orelse pending_result node then |
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
478 |
let |
52775
e0169f13bd37
keep memo_exec execution running, which is important to cancel goal forks eventually;
wenzelm
parents:
52774
diff
changeset
|
479 |
fun body () = |
59347 | 480 |
(if forall finished_import deps then |
59198
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
481 |
iterate_entries (fn (_, opt_exec) => fn () => |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
482 |
(case opt_exec of |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
483 |
SOME exec => |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
484 |
if Execution.is_running execution_id |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
485 |
then SOME (Command.exec execution_id exec) |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
486 |
else NONE |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
487 |
| NONE => NONE)) node () |
59347 | 488 |
else ()) |
489 |
handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn); |
|
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
490 |
val future = |
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52772
diff
changeset
|
491 |
(singleton o Future.forks) |
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:
59086
diff
changeset
|
492 |
{name = "theory:" ^ name, |
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:
59086
diff
changeset
|
493 |
group = SOME (Future.new_group NONE), |
59198
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
494 |
deps = Future.task_of delay_request' :: maps (the_list o #2 o #2) deps, |
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:
59086
diff
changeset
|
495 |
pri = 0, interrupts = false} body; |
59198
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
496 |
in (node, SOME (Future.task_of future)) end |
c73933e07c03
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
wenzelm
parents:
59193
diff
changeset
|
497 |
else (node, NONE)); |
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52797
diff
changeset
|
498 |
val execution' = |
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:
59086
diff
changeset
|
499 |
{version_id = version_id, execution_id = execution_id, delay_request = delay_request'}; |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
500 |
in (versions, blobs, commands, execution') end)); |
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset
|
501 |
|
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset
|
502 |
|
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
503 |
|
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset
|
504 |
(** document update **) |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
505 |
|
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
506 |
(* exec state assignment *) |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
507 |
|
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
508 |
type assign_update = Command.exec option Inttab.table; (*command id -> exec*) |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
509 |
|
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
510 |
val assign_update_empty: assign_update = Inttab.empty; |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
511 |
fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
512 |
fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
513 |
|
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
514 |
fun assign_update_new upd (tab: assign_update) = |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
515 |
Inttab.update_new upd tab |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
516 |
handle Inttab.DUP dup => err_dup "exec state assignment" dup; |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
517 |
|
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
518 |
fun assign_update_result (tab: assign_update) = |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
519 |
Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab []; |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
520 |
|
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
521 |
|
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
522 |
(* update *) |
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
523 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
524 |
local |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
525 |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset
|
526 |
fun init_theory deps node span = |
47335 | 527 |
let |
54526 | 528 |
val master_dir = master_directory node; |
529 |
val header = read_header node span; |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset
|
530 |
val imports = #imports header; |
59716 | 531 |
|
532 |
fun maybe_end_theory pos st = |
|
533 |
SOME (Toplevel.end_theory pos st) |
|
534 |
handle ERROR msg => (Output.error_message msg; NONE); |
|
535 |
val parents_reports = |
|
536 |
imports |> map_filter (fn (import, pos) => |
|
54516 | 537 |
(case loaded_theory import of |
59716 | 538 |
NONE => |
539 |
maybe_end_theory pos |
|
52536 | 540 |
(case get_result (snd (the (AList.lookup (op =) deps import))) of |
541 |
NONE => Toplevel.toplevel |
|
59716 | 542 |
| SOME eval => Command.eval_result_state eval) |
543 |
| some => some) |
|
544 |
|> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))); |
|
545 |
||
546 |
val parents = |
|
547 |
if null parents_reports then [Thy_Info.get_theory "Pure"] else map #1 parents_reports; |
|
548 |
val _ = Position.reports (map #2 parents_reports); |
|
56208 | 549 |
in Resources.begin_theory master_dir header parents end; |
47335 | 550 |
|
47407 | 551 |
fun check_theory full name node = |
54516 | 552 |
is_some (loaded_theory name) orelse |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59702
diff
changeset
|
553 |
null (#errors (get_header node)) andalso (not full orelse is_some (get_result node)); |
47335 | 554 |
|
58923 | 555 |
fun last_common keywords state node_required node0 node = |
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset
|
556 |
let |
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
557 |
fun update_flags prev (visible, initial) = |
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
558 |
let |
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
559 |
val visible' = visible andalso prev <> visible_last node; |
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
560 |
val initial' = initial andalso |
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
561 |
(case prev of |
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
562 |
NONE => true |
59735 | 563 |
| SOME command_id => the_command_name state command_id <> Thy_Header.theoryN); |
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
564 |
in (visible', initial') end; |
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
565 |
|
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
566 |
fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) = |
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
567 |
if ok then |
47630 | 568 |
let |
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
569 |
val flags' as (visible', _) = update_flags prev flags; |
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
570 |
val ok' = |
52586 | 571 |
(case (lookup_entry node0 command_id, opt_exec) of |
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
572 |
(SOME (eval0, _), SOME (eval, _)) => |
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
573 |
Command.eval_eq (eval0, eval) andalso |
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
574 |
(visible' orelse node_required orelse Command.eval_running eval) |
52586 | 575 |
| _ => false); |
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
576 |
val assign_update' = assign_update |> ok' ? |
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
577 |
(case opt_exec of |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
578 |
SOME (eval, prints) => |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
579 |
let |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
580 |
val command_visible = visible_command node command_id; |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52849
diff
changeset
|
581 |
val command_overlays = overlays node command_id; |
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
582 |
val command_name = the_command_name state command_id; |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
583 |
in |
58923 | 584 |
(case |
585 |
Command.print command_visible command_overlays keywords command_name eval prints |
|
586 |
of |
|
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
587 |
SOME prints' => assign_update_new (command_id, SOME (eval, prints')) |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
588 |
| NONE => I) |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
589 |
end |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
590 |
| NONE => I); |
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
591 |
in SOME (prev, ok', flags', assign_update') end |
47630 | 592 |
else NONE; |
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
593 |
val (common, ok, flags, assign_update') = |
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
594 |
iterate_entries get_common node (NONE, true, (true, true), assign_update_empty); |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
595 |
val (common', flags') = |
52784
4ba2e8b9972f
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents:
52776
diff
changeset
|
596 |
if ok then |
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
597 |
let val last = Entries.get_after (get_entries node) common |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
598 |
in (last, update_flags last flags) end |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
599 |
else (common, flags); |
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset
|
600 |
in (assign_update', common', flags') end; |
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
601 |
|
52534 | 602 |
fun illegal_init _ = error "Illegal theory header after end of theory"; |
603 |
||
58923 | 604 |
fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) = |
47407 | 605 |
if not proper_init andalso is_none init then NONE |
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
606 |
else |
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset
|
607 |
let |
52534 | 608 |
val (_, (eval, _)) = command_exec; |
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52849
diff
changeset
|
609 |
|
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52849
diff
changeset
|
610 |
val command_visible = visible_command node command_id'; |
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52849
diff
changeset
|
611 |
val command_overlays = overlays node command_id'; |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59687
diff
changeset
|
612 |
val (command_name, blob_digests, blobs_index, span0) = the_command state command_id'; |
56447
1e77ed11f2f7
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents:
56208
diff
changeset
|
613 |
val blobs = map (resolve_blob state) blob_digests; |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
614 |
val span = Lazy.force span0; |
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
615 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54516
diff
changeset
|
616 |
val eval' = |
58934
385a4cc7426f
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
wenzelm
parents:
58928
diff
changeset
|
617 |
Command.eval keywords (master_directory node) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59687
diff
changeset
|
618 |
(fn () => the_default illegal_init init span) (blobs, blobs_index) span eval; |
58923 | 619 |
val prints' = |
620 |
perhaps (Command.print command_visible command_overlays keywords command_name eval') []; |
|
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
621 |
val exec' = (eval', prints'); |
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset
|
622 |
|
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
623 |
val assign_update' = assign_update_new (command_id', SOME exec') assign_update; |
59735 | 624 |
val init' = if command_name = Thy_Header.theoryN then NONE else init; |
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset
|
625 |
in SOME (assign_update', (command_id', (eval', prints')), init') end; |
52602
00170ef1dc39
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents:
52600
diff
changeset
|
626 |
|
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
627 |
fun removed_execs node0 (command_id, exec_ids) = |
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
628 |
subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); |
52602
00170ef1dc39
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents:
52600
diff
changeset
|
629 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
630 |
in |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
631 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
632 |
fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () => |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
633 |
let |
52536 | 634 |
val old_version = the_version state old_version_id; |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
635 |
val new_version = |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
636 |
timeit "Document.edit_nodes" |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
637 |
(fn () => old_version |> fold edit_nodes edits |> edit_keywords edits); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
638 |
|
44544
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset
|
639 |
val nodes = nodes_of new_version; |
52776 | 640 |
val required = make_required nodes; |
641 |
val required0 = make_required (nodes_of old_version); |
|
52772 | 642 |
val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty; |
44544
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset
|
643 |
|
47628 | 644 |
val updated = timeit "Document.update" (fn () => |
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset
|
645 |
nodes |> String_Graph.schedule |
44199
e38885e3ea60
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset
|
646 |
(fn deps => fn (name, node) => |
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset
|
647 |
(singleton o Future.forks) |
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset
|
648 |
{name = "Document.update", group = NONE, |
52716 | 649 |
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} |
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
650 |
(fn () => |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
651 |
timeit ("Document.update " ^ name) (fn () => |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
652 |
Runtime.exn_trace_system (fn () => |
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset
|
653 |
let |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59085
diff
changeset
|
654 |
val keywords = the_default (Session.get_keywords ()) (get_keywords node); |
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
655 |
val imports = map (apsnd Future.join) deps; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
656 |
val imports_result_changed = exists (#4 o #1 o #2) imports; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
657 |
val node_required = Symtab.defined required name; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
658 |
in |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
659 |
if Symtab.defined edited name orelse visible_node node orelse |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
660 |
imports_result_changed orelse Symtab.defined required0 name <> node_required |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
661 |
then |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
662 |
let |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
663 |
val node0 = node_of old_version name; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
664 |
val init = init_theory imports node; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
665 |
val proper_init = |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
666 |
check_theory false name node andalso |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
667 |
forall (fn (name, (_, node)) => check_theory true name node) imports; |
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset
|
668 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
669 |
val (print_execs, common, (still_visible, initial)) = |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
670 |
if imports_result_changed then (assign_update_empty, NONE, (true, true)) |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
671 |
else last_common keywords state node_required node0 node; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
672 |
val common_command_exec = the_default_entry node common; |
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset
|
673 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
674 |
val (updated_execs, (command_id', (eval', _)), _) = |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
675 |
(print_execs, common_command_exec, if initial then SOME init else NONE) |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
676 |
|> (still_visible orelse node_required) ? |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
677 |
iterate_entries_after common |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
678 |
(fn ((prev, id), _) => fn res => |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
679 |
if not node_required andalso prev = visible_last node then NONE |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
680 |
else new_exec keywords state node proper_init id res) node; |
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset
|
681 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
682 |
val assigned_execs = |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
683 |
(node0, updated_execs) |-> iterate_entries_after common |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
684 |
(fn ((_, command_id0), exec0) => fn res => |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
685 |
if is_none exec0 then NONE |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
686 |
else if assign_update_defined updated_execs command_id0 then SOME res |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
687 |
else SOME (assign_update_new (command_id0, NONE) res)); |
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset
|
688 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
689 |
val last_exec = |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
690 |
if command_id' = Document_ID.none then NONE else SOME command_id'; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
691 |
val result = |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
692 |
if is_none last_exec orelse is_some (after_entry node last_exec) then NONE |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
693 |
else SOME eval'; |
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset
|
694 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
695 |
val assign_update = assign_update_result assigned_execs; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
696 |
val removed = maps (removed_execs node0) assign_update; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
697 |
val _ = List.app Execution.cancel removed; |
52602
00170ef1dc39
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents:
52600
diff
changeset
|
698 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
699 |
val node' = node |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
700 |
|> assign_update_apply assigned_execs |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
701 |
|> set_result result; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
702 |
val assigned_node = SOME (name, node'); |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
703 |
val result_changed = changed_result node0 node'; |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
704 |
in ((removed, assign_update, assigned_node, result_changed), node') end |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
705 |
else (([], [], NONE, false), node) |
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
706 |
end)))) |
47628 | 707 |
|> Future.joins |> map #1); |
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset
|
708 |
|
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
709 |
val removed = maps #1 updated; |
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
710 |
val assign_update = maps #2 updated; |
52602
00170ef1dc39
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents:
52600
diff
changeset
|
711 |
val assigned_nodes = map_filter #3 updated; |
00170ef1dc39
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents:
52600
diff
changeset
|
712 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
713 |
val state' = state |
52602
00170ef1dc39
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents:
52600
diff
changeset
|
714 |
|> define_version new_version_id (fold put_node assigned_nodes new_version); |
00170ef1dc39
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents:
52600
diff
changeset
|
715 |
|
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
58934
diff
changeset
|
716 |
in (removed, assign_update, state') end); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
717 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
718 |
end; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
719 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
720 |
|
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
721 |
|
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
722 |
(** global state **) |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
723 |
|
52508 | 724 |
val global_state = Synchronized.var "Document.global_state" init_state; |
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
725 |
|
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
726 |
fun state () = Synchronized.value global_state; |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
727 |
val change_state = Synchronized.change global_state; |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
728 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
729 |
end; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
730 |