21 Edits of (command_id option * command_id option) list | |
21 Edits of (command_id option * command_id option) list | |
22 Header of node_header |
22 Header of node_header |
23 type edit = string * node_edit |
23 type edit = string * node_edit |
24 type state |
24 type state |
25 val init_state: state |
25 val init_state: state |
26 val get_theory: state -> version_id -> Position.T -> string -> theory |
26 val join_commands: state -> unit |
27 val cancel_execution: state -> unit -> unit |
27 val cancel_execution: state -> unit -> unit |
28 val define_command: command_id -> string -> state -> state |
28 val define_command: command_id -> string -> state -> state |
29 val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state |
29 val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state |
30 val execute: version_id -> state -> state |
30 val execute: version_id -> state -> state |
31 val state: unit -> state |
31 val state: unit -> state |
59 structure Entries = Linear_Set(type key = command_id val ord = int_ord); |
59 structure Entries = Linear_Set(type key = command_id val ord = int_ord); |
60 |
60 |
61 abstype node = Node of |
61 abstype node = Node of |
62 {header: node_header, |
62 {header: node_header, |
63 entries: exec_id option Entries.T, (*command entries with excecutions*) |
63 entries: exec_id option Entries.T, (*command entries with excecutions*) |
64 last: exec_id} (*last entry with main result*) |
64 result: Toplevel.state lazy} |
65 and version = Version of node Graph.T (*development graph wrt. static imports*) |
65 and version = Version of node Graph.T (*development graph wrt. static imports*) |
66 with |
66 with |
67 |
67 |
68 fun make_node (header, entries, last) = |
68 fun make_node (header, entries, result) = |
69 Node {header = header, entries = entries, last = last}; |
69 Node {header = header, entries = entries, result = result}; |
70 |
70 |
71 fun map_node f (Node {header, entries, last}) = |
71 fun map_node f (Node {header, entries, result}) = |
72 make_node (f (header, entries, last)); |
72 make_node (f (header, entries, result)); |
73 |
73 |
74 fun get_header (Node {header, ...}) = header; |
74 fun get_header (Node {header, ...}) = header; |
75 fun set_header header = map_node (fn (_, entries, last) => (header, entries, last)); |
75 fun set_header header = map_node (fn (_, entries, result) => (header, entries, result)); |
76 |
76 |
77 fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last); |
77 fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result); |
78 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; |
78 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; |
79 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; |
79 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; |
80 |
80 |
81 fun get_last (Node {last, ...}) = last; |
81 fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result); |
82 fun set_last last = map_node (fn (header, entries, _) => (header, entries, last)); |
82 fun set_result result = map_node (fn (header, entries, _) => (header, entries, result)); |
83 |
83 |
84 val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id); |
84 val empty_exec = Lazy.value Toplevel.toplevel; |
85 val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id)); |
85 val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec); |
|
86 val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec)); |
86 |
87 |
87 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; |
88 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; |
88 fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes; |
89 fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes; |
89 fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f; |
90 fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f; |
90 |
91 |
141 val (header', nodes'') = |
142 val (header', nodes'') = |
142 (header, Graph.add_deps_acyclic (name, parents) nodes') |
143 (header, Graph.add_deps_acyclic (name, parents) nodes') |
143 handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes'); |
144 handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes'); |
144 in Graph.map_node name (set_header header') nodes'' end); |
145 in Graph.map_node name (set_header header') nodes'' end); |
145 |
146 |
146 fun put_node name node (Version nodes) = |
147 fun put_node (name, node) (Version nodes) = |
147 Version (nodes |
148 Version (nodes |
148 |> Graph.default_node (name, empty_node) |
149 |> Graph.default_node (name, empty_node) |
149 |> Graph.map_node name (K node)); |
150 |> Graph.map_node name (K node)); |
150 |
151 |
151 end; |
152 end; |
168 make_state (f (versions, commands, execs, execution)); |
169 make_state (f (versions, commands, execs, execution)); |
169 |
170 |
170 val init_state = |
171 val init_state = |
171 make_state (Inttab.make [(no_id, empty_version)], |
172 make_state (Inttab.make [(no_id, empty_version)], |
172 Inttab.make [(no_id, Future.value Toplevel.empty)], |
173 Inttab.make [(no_id, Future.value Toplevel.empty)], |
173 Inttab.make [(no_id, Lazy.value Toplevel.toplevel)], |
174 Inttab.make [(no_id, empty_exec)], |
174 []); |
175 []); |
175 |
176 |
176 |
177 |
177 (* document versions *) |
178 (* document versions *) |
178 |
179 |
211 Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands (); |
212 Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands (); |
212 |
213 |
213 |
214 |
214 (* command executions *) |
215 (* command executions *) |
215 |
216 |
216 fun define_exec (id: exec_id) exec = |
217 fun define_exec (exec_id, exec) = |
217 map_state (fn (versions, commands, execs, execution) => |
218 map_state (fn (versions, commands, execs, execution) => |
218 let val execs' = Inttab.update_new (id, exec) execs |
219 let val execs' = Inttab.update_new (exec_id, exec) execs |
219 handle Inttab.DUP dup => err_dup "command execution" dup |
220 handle Inttab.DUP dup => err_dup "command execution" dup |
220 in (versions, commands, execs', execution) end); |
221 in (versions, commands, execs', execution) end); |
221 |
222 |
222 fun the_exec (State {execs, ...}) (id: exec_id) = |
223 fun the_exec (State {execs, ...}) exec_id = |
223 (case Inttab.lookup execs id of |
224 (case Inttab.lookup execs exec_id of |
224 NONE => err_undef "command execution" id |
225 NONE => err_undef "command execution" exec_id |
225 | SOME exec => exec); |
226 | SOME exec => exec); |
226 |
|
227 fun get_theory state version_id pos name = |
|
228 let |
|
229 val last = get_last (node_of (the_version state version_id) name); |
|
230 val st = |
|
231 (case Lazy.peek (the_exec state last) of |
|
232 SOME result => Exn.release result |
|
233 | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos)); |
|
234 in Toplevel.end_theory pos st end; |
|
235 |
227 |
236 |
228 |
237 (* document execution *) |
229 (* document execution *) |
238 |
230 |
239 fun cancel_execution (State {execution, ...}) = |
231 fun cancel_execution (State {execution, ...}) = |
322 fun is_changed node' ((_, id), exec) = |
314 fun is_changed node' ((_, id), exec) = |
323 (case try (the_entry node') id of |
315 (case try (the_entry node') id of |
324 NONE => true |
316 NONE => true |
325 | SOME exec' => exec' <> exec); |
317 | SOME exec' => exec' <> exec); |
326 |
318 |
327 fun new_exec node_info (id: command_id) (exec_id, updates, state) = |
319 fun new_exec node_info (command, command_id) (assigns, execs, exec) = |
328 let |
320 let |
329 val exec = the_exec state exec_id; |
|
330 val exec_id' = new_id (); |
321 val exec_id' = new_id (); |
331 val future_tr = the_command state id; |
|
332 val exec' = |
322 val exec' = |
333 Lazy.lazy (fn () => |
323 Lazy.lazy (fn () => |
334 let |
324 let |
335 val st = Lazy.force exec; |
325 val tr = Toplevel.put_id (print_id exec_id') (Future.join command); (* FIXME Future.join_finished !? *) |
336 val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr); |
326 val st = Lazy.force exec; (* FIXME Lazy.force_finished !? *) |
337 in run_command node_info exec_tr st end); |
327 in run_command node_info tr st end); |
338 val state' = define_exec exec_id' exec' state; |
328 in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end; |
339 in (exec_id', (id, exec_id') :: updates, state') end; |
|
340 |
329 |
341 in |
330 in |
342 |
331 |
343 fun edit (old_id: version_id) (new_id: version_id) edits state = |
332 fun edit (old_id: version_id) (new_id: version_id) edits state = |
344 let |
333 let |
345 val old_version = the_version state old_id; |
334 val old_version = the_version state old_id; |
346 val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) |
335 val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) |
347 val new_version = fold edit_nodes edits old_version; |
336 val new_version = fold edit_nodes edits old_version; |
348 |
337 |
349 fun update_node name (rev_updates, version, st) = |
338 (* FIXME futures *) |
350 let |
339 val updates = |
351 val node = node_of version name; |
340 nodes_of new_version |> Graph.schedule |
352 val header = get_header node; |
341 (fn _ => fn (name, node) => |
353 in |
342 (case first_entry NONE (is_changed (node_of old_version name)) node of |
354 (case first_entry NONE (is_changed (node_of old_version name)) node of |
343 NONE => (([], [], []), node) |
355 NONE => (rev_updates, version, st) |
344 | SOME ((prev, id), _) => |
356 | SOME ((prev, id), _) => |
345 let |
357 let |
346 val prev_exec = |
358 val prev_exec = |
347 (case prev of |
359 (case prev of |
348 NONE => no_id |
360 NONE => no_id |
349 | SOME prev_id => the_default no_id (the_entry node prev_id)); |
361 | SOME prev_id => the_default no_id (the_entry node prev_id)); |
350 val (assigns, execs, result) = |
362 val (last, rev_upds, st') = |
351 fold_entries (SOME id) |
363 fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st); |
352 (new_exec (name, get_header node) o `(the_command state) o #2 o #1) |
364 val node' = node |> fold update_entry rev_upds |> set_last last; |
353 node ([], [], the_exec state prev_exec); |
365 in (rev_upds @ rev_updates, put_node name node' version, st') end) |
354 val node' = node |> fold update_entry assigns |> set_result result; |
366 end; |
355 in ((assigns, execs, [(name, node')]), node') end)) |
367 |
356 |> map #1; |
368 (* FIXME Graph.schedule *) |
357 |
369 val (rev_updates, new_version', state') = |
358 val state' = state |
370 fold update_node (node_names_of new_version) ([], new_version, state); |
359 |> fold (fold define_exec o #2) updates |
371 val state'' = define_version new_id new_version' state'; |
360 |> define_version new_id (fold (fold put_node o #3) updates new_version); |
372 |
361 |
373 val _ = join_commands state''; (* FIXME async!? *) |
362 in (maps #1 (rev updates), state') end; |
374 in (rev rev_updates, state'') end; |
|
375 |
363 |
376 end; |
364 end; |
377 |
365 |
378 |
366 |
379 (* execute *) |
367 (* execute *) |