27 val define_command: command_id -> string -> state -> state |
27 val define_command: command_id -> string -> state -> state |
28 val join_commands: state -> unit |
28 val join_commands: state -> unit |
29 val cancel_execution: state -> Future.task list |
29 val cancel_execution: state -> Future.task list |
30 val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state |
30 val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state |
31 val edit: version_id -> version_id -> edit list -> state -> |
31 val edit: version_id -> version_id -> edit list -> state -> |
32 ((command_id * exec_id) list * (string * command_id option) list) * state |
32 ((command_id * exec_id option) list * (string * command_id option) list) * state |
33 val execute: version_id -> state -> state |
33 val execute: version_id -> state -> state |
34 val state: unit -> state |
34 val state: unit -> state |
35 val change_state: (state -> state) -> unit |
35 val change_state: (state -> state) -> unit |
36 end; |
36 end; |
37 |
37 |
138 Header of node_header | |
138 Header of node_header | |
139 Perspective of command_id list; |
139 Perspective of command_id list; |
140 |
140 |
141 type edit = string * node_edit; |
141 type edit = string * node_edit; |
142 |
142 |
|
143 fun next_entry (Node {entries, ...}) id = |
|
144 (case Entries.lookup entries id of |
|
145 NONE => err_undef "command entry" id |
|
146 | SOME (_, next) => next); |
|
147 |
143 fun the_entry (Node {entries, ...}) id = |
148 fun the_entry (Node {entries, ...}) id = |
144 (case Entries.lookup entries id of |
149 (case Entries.lookup entries id of |
145 NONE => err_undef "command entry" id |
150 NONE => err_undef "command entry" id |
146 | SOME (exec, _) => exec); |
151 | SOME (exec, _) => exec); |
147 |
152 |
148 fun is_last_entry (Node {entries, ...}) id = |
153 fun the_default_entry node (SOME id) = the_default no_id (the_entry node id) |
149 (case Entries.lookup entries id of |
154 | the_default_entry _ NONE = no_id; |
150 SOME (_, SOME _) => false |
|
151 | _ => true); |
|
152 |
155 |
153 fun update_entry id exec_id = |
156 fun update_entry id exec_id = |
154 map_entries (Entries.update (id, SOME exec_id)); |
157 map_entries (Entries.update (id, SOME exec_id)); |
155 |
158 |
156 fun reset_after id entries = |
159 fun reset_after id entries = |
206 (header, Graph.add_deps_acyclic (name, parents) nodes2) |
209 (header, Graph.add_deps_acyclic (name, parents) nodes2) |
207 handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); |
210 handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); |
208 in Graph.map_node name (set_header header') nodes3 end |
211 in Graph.map_node name (set_header header') nodes3 end |
209 |> touch_node name |
212 |> touch_node name |
210 | Perspective perspective => |
213 | Perspective perspective => |
211 update_node name (set_perspective perspective) nodes); |
214 nodes |
|
215 |> update_node name (set_perspective perspective) |
|
216 |> touch_node name (* FIXME more precise!?! *)); |
212 |
217 |
213 end; |
218 end; |
214 |
219 |
215 fun put_node (name, node) (Version nodes) = |
220 fun put_node (name, node) (Version nodes) = |
216 Version (update_node name (K node) nodes); |
221 Version (update_node name (K node) nodes); |
416 val new_version = fold edit_nodes edits old_version; |
424 val new_version = fold edit_nodes edits old_version; |
417 |
425 |
418 val updated = |
426 val updated = |
419 nodes_of new_version |> Graph.schedule |
427 nodes_of new_version |> Graph.schedule |
420 (fn deps => fn (name, node) => |
428 (fn deps => fn (name, node) => |
421 if not (is_touched node) then Future.value (([], []), node) |
429 if not (is_touched node) then Future.value (([], [], []), node) |
422 else |
430 else |
423 (case first_entry NONE (is_changed (node_of old_version name)) node of |
431 let |
424 NONE => Future.value (([], []), set_touched false node) |
432 val node0 = node_of old_version name; |
425 | SOME ((prev, id), _) => |
433 fun init () = init_theory deps name node; |
426 let |
434 in |
427 fun init () = init_theory deps name node; |
435 (case first_entry NONE (after_perspective node orf needs_update node0) node of |
428 in |
436 NONE => Future.value (([], [], []), set_touched false node) |
|
437 | SOME ((prev, id), _) => |
429 (singleton o Future.forks) |
438 (singleton o Future.forks) |
430 {name = "Document.edit", group = NONE, |
439 {name = "Document.edit", group = NONE, |
431 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} |
440 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} |
432 (fn () => |
441 (fn () => |
433 let |
442 let |
434 val prev_exec = |
443 val (execs, exec) = |
435 (case prev of |
444 fold_entries (SOME id) |
436 NONE => no_id |
445 (fn entry1 as ((_, id1), _) => fn res => |
437 | SOME prev_id => the_default no_id (the_entry node prev_id)); |
446 if after_perspective node entry1 then NONE |
438 val (execs, last_exec as (last_id, _)) = |
447 else SOME (new_exec state init id1 res)) |
439 fold_entries (SOME id) (new_exec state init o #2 o #1) |
448 node ([], the_exec state (the_default_entry node prev)); |
440 node ([], the_exec state prev_exec); |
449 |
441 val node' = |
450 val no_execs = |
|
451 if can (the_entry node0) id then |
|
452 fold_entries (SOME id) |
|
453 (fn ((_, id0), exec0) => fn res => |
|
454 if is_none exec0 then NONE |
|
455 else if exists (fn (_, (id1, _)) => id0 = id1) execs then SOME res |
|
456 else SOME (id0 :: res)) node0 [] |
|
457 else []; |
|
458 |
|
459 val node1 = |
442 fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id) |
460 fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id) |
443 execs node; |
461 execs node; |
|
462 val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec); |
444 val result = |
463 val result = |
445 if is_last_entry node' last_id |
464 if is_some last_exec andalso is_none (next_entry node1 (the last_exec)) |
446 then Lazy.map #1 (#2 last_exec) |
465 then Lazy.map #1 (#2 exec) |
447 else no_result; |
466 else no_result; |
448 val node'' = node' |
467 val node2 = node1 |
449 |> set_last_exec (if last_id = no_id then NONE else SOME last_id) |
468 |> set_last_exec last_exec |
450 |> set_result result |
469 |> set_result result |
451 |> set_touched false; |
470 |> set_touched false; |
452 in ((execs, [(name, node'')]), node'') end) |
471 in ((no_execs, execs, [(name, node2)]), node2) end)) |
453 end)) |
472 end) |
454 |> Future.joins |> map #1 |> rev; (* FIXME why rev? *) |
473 |> Future.joins |> map #1; |
455 |
474 |
456 val updated_nodes = maps #2 updated; |
475 val command_execs = |
457 val assignment = map (fn (exec_id, (command_id, _)) => (command_id, exec_id)) (maps #1 updated); |
476 map (rpair NONE) (maps #1 updated) @ |
|
477 map (fn (exec_id, (command_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); |
|
478 val updated_nodes = maps #3 updated; |
458 val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes; |
479 val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes; |
459 |
480 |
460 val state' = state |
481 val state' = state |
461 |> fold (fold define_exec o #1) updated |
482 |> fold (fold define_exec o #2) updated |
462 |> define_version new_id (fold put_node updated_nodes new_version); |
483 |> define_version new_id (fold put_node updated_nodes new_version); |
463 in ((assignment, last_execs), state') end; |
484 in ((command_execs, last_execs), state') end; |
464 |
485 |
465 end; |
486 end; |
466 |
487 |
467 |
488 |
468 (* execute *) |
489 (* execute *) |
488 nodes_of version |> Graph.schedule |
509 nodes_of version |> Graph.schedule |
489 (fn deps => fn (name, node) => |
510 (fn deps => fn (name, node) => |
490 (singleton o Future.forks) |
511 (singleton o Future.forks) |
491 {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)), |
512 {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)), |
492 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true} |
513 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true} |
493 (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node)); |
514 (fold_entries NONE |
|
515 (fn entry as (_, exec) => fn () => SOME (force_exec node exec)) node)); |
494 |
516 |
495 in (versions, commands, execs, execution) end); |
517 in (versions, commands, execs, execution) end); |
496 |
518 |
497 |
519 |
498 |
520 |