60 type node_header = (string * string list * (string * bool) list) Exn.result; |
60 type node_header = (string * string list * (string * bool) list) Exn.result; |
61 type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*) |
61 type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*) |
62 structure Entries = Linear_Set(type key = command_id val ord = int_ord); |
62 structure Entries = Linear_Set(type key = command_id val ord = int_ord); |
63 |
63 |
64 abstype node = Node of |
64 abstype node = Node of |
65 {header: node_header, |
65 {touched: bool, |
|
66 header: node_header, |
66 perspective: perspective, |
67 perspective: perspective, |
67 entries: exec_id option Entries.T, (*command entries with excecutions*) |
68 entries: exec_id option Entries.T, (*command entries with excecutions*) |
68 result: Toplevel.state lazy} |
69 result: Toplevel.state lazy} |
69 and version = Version of node Graph.T (*development graph wrt. static imports*) |
70 and version = Version of node Graph.T (*development graph wrt. static imports*) |
70 with |
71 with |
71 |
72 |
72 fun make_node (header, perspective, entries, result) = |
73 fun make_node (touched, header, perspective, entries, result) = |
73 Node {header = header, perspective = perspective, entries = entries, result = result}; |
74 Node {touched = touched, header = header, perspective = perspective, |
74 |
75 entries = entries, result = result}; |
75 fun map_node f (Node {header, perspective, entries, result}) = |
76 |
76 make_node (f (header, perspective, entries, result)); |
77 fun map_node f (Node {touched, header, perspective, entries, result}) = |
|
78 make_node (f (touched, header, perspective, entries, result)); |
77 |
79 |
78 fun make_perspective ids : perspective = |
80 fun make_perspective ids : perspective = |
79 (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids); |
81 (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids); |
80 |
82 |
81 val no_perspective = make_perspective []; |
83 val no_perspective = make_perspective []; |
82 val no_print = Lazy.value (); |
84 val no_print = Lazy.value (); |
83 val no_result = Lazy.value Toplevel.toplevel; |
85 val no_result = Lazy.value Toplevel.toplevel; |
84 |
86 |
85 val empty_node = |
87 val empty_node = |
86 make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result); |
88 make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result); |
87 |
89 |
88 val clear_node = |
90 val clear_node = |
89 map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result)); |
91 map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result)); |
90 |
92 |
91 |
93 |
92 (* basic components *) |
94 (* basic components *) |
|
95 |
|
96 fun get_touched (Node {touched, ...}) = touched; |
|
97 fun set_touched touched = |
|
98 map_node (fn (_, header, perspective, entries, result) => |
|
99 (touched, header, perspective, entries, result)); |
93 |
100 |
94 fun get_header (Node {header, ...}) = header; |
101 fun get_header (Node {header, ...}) = header; |
95 fun set_header header = |
102 fun set_header header = |
96 map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result)); |
103 map_node (fn (touched, _, perspective, entries, result) => |
|
104 (touched, header, perspective, entries, result)); |
97 |
105 |
98 fun get_perspective (Node {perspective, ...}) = perspective; |
106 fun get_perspective (Node {perspective, ...}) = perspective; |
99 fun set_perspective ids = |
107 fun set_perspective ids = |
100 map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result)); |
108 map_node (fn (touched, header, _, entries, result) => |
101 |
109 (touched, header, make_perspective ids, entries, result)); |
102 fun map_entries f (Node {header, perspective, entries, result}) = |
110 |
103 make_node (header, perspective, f entries, result); |
111 fun map_entries f = |
|
112 map_node (fn (touched, header, perspective, entries, result) => |
|
113 (touched, header, perspective, f entries, result)); |
104 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; |
114 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; |
105 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; |
115 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; |
106 |
116 |
107 fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result); |
117 fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result); |
108 fun set_result result = |
118 fun set_result result = |
109 map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); |
119 map_node (fn (touched, header, perspective, entries, _) => |
|
120 (touched, header, perspective, entries, result)); |
110 |
121 |
111 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; |
122 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; |
112 fun default_node name = Graph.default_node (name, empty_node); |
123 fun default_node name = Graph.default_node (name, empty_node); |
113 fun update_node name f = default_node name #> Graph.map_node name f; |
124 fun update_node name f = default_node name #> Graph.map_node name f; |
114 |
125 |
384 val new_version = fold edit_nodes edits old_version; |
403 val new_version = fold edit_nodes edits old_version; |
385 |
404 |
386 val updates = |
405 val updates = |
387 nodes_of new_version |> Graph.schedule |
406 nodes_of new_version |> Graph.schedule |
388 (fn deps => fn (name, node) => |
407 (fn deps => fn (name, node) => |
389 (case first_entry NONE (is_changed (node_of old_version name)) node of |
408 if not (get_touched node) then Future.value (([], [], []), node) |
390 NONE => Future.value (([], [], []), node) |
409 else |
391 | SOME ((prev, id), _) => |
410 (case first_entry NONE (is_changed (node_of old_version name)) node of |
392 let |
411 NONE => Future.value (([], [], []), set_touched false node) |
393 fun init () = init_theory deps name node; |
412 | SOME ((prev, id), _) => |
394 in |
413 let |
395 (singleton o Future.forks) |
414 fun init () = init_theory deps name node; |
396 {name = "Document.edit", group = NONE, |
415 in |
397 deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false} |
416 (singleton o Future.forks) |
398 (fn () => |
417 {name = "Document.edit", group = NONE, |
399 let |
418 deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false} |
400 val prev_exec = |
419 (fn () => |
401 (case prev of |
420 let |
402 NONE => no_id |
421 val prev_exec = |
403 | SOME prev_id => the_default no_id (the_entry node prev_id)); |
422 (case prev of |
404 val (assigns, execs, last_exec) = |
423 NONE => no_id |
405 fold_entries (SOME id) (new_exec state init o #2 o #1) |
424 | SOME prev_id => the_default no_id (the_entry node prev_id)); |
406 node ([], [], #2 (the_exec state prev_exec)); |
425 val (assigns, execs, last_exec) = |
407 val node' = node |
426 fold_entries (SOME id) (new_exec state init o #2 o #1) |
408 |> fold update_entry assigns |
427 node ([], [], #2 (the_exec state prev_exec)); |
409 |> set_result (Lazy.map #1 last_exec); |
428 val node' = node |
410 in ((assigns, execs, [(name, node')]), node') end) |
429 |> fold update_entry assigns |
411 end)) |
430 |> set_result (Lazy.map #1 last_exec) |
|
431 |> set_touched false; |
|
432 in ((assigns, execs, [(name, node')]), node') end) |
|
433 end)) |
412 |> Future.joins |> map #1; |
434 |> Future.joins |> map #1; |
413 |
435 |
414 val state' = state |
436 val state' = state |
415 |> fold (fold define_exec o #2) updates |
437 |> fold (fold define_exec o #2) updates |
416 |> define_version new_id (fold (fold put_node o #3) updates new_version); |
438 |> define_version new_id (fold (fold put_node o #3) updates new_version); |