--- a/src/Pure/PIDE/document.ML Mon Apr 09 17:38:39 2012 +0200
+++ b/src/Pure/PIDE/document.ML Mon Apr 09 19:50:04 2012 +0200
@@ -66,20 +66,18 @@
val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
abstype node = Node of
- {touched: bool,
- header: node_header,
+ {header: node_header,
perspective: perspective,
entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*)
result: exec}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (touched, header, perspective, entries, result) =
- Node {touched = touched, header = header, perspective = perspective,
- entries = entries, result = result};
+fun make_node (header, perspective, entries, result) =
+ Node {header = header, perspective = perspective, entries = entries, result = result};
-fun map_node f (Node {touched, header, perspective, entries, result}) =
- make_node (f (touched, header, perspective, entries, result));
+fun map_node f (Node {header, perspective, entries, result}) =
+ make_node (f (header, perspective, entries, result));
fun make_perspective command_ids : perspective =
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
@@ -87,35 +85,26 @@
val no_header = Exn.Exn (ERROR "Bad theory header");
val no_perspective = make_perspective [];
-val empty_node = make_node (false, no_header, no_perspective, Entries.empty, no_exec);
-val clear_node = map_node (fn (_, header, _, _, _) =>
- (false, header, no_perspective, Entries.empty, no_exec));
+val empty_node = make_node (no_header, no_perspective, Entries.empty, no_exec);
+val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_exec));
(* basic components *)
-fun is_touched (Node {touched, ...}) = touched;
-fun set_touched touched =
- map_node (fn (_, header, perspective, entries, result) =>
- (touched, header, perspective, entries, result));
-
fun get_header (Node {header, ...}) = header;
fun set_header header =
- map_node (fn (touched, _, perspective, entries, result) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective ids =
- map_node (fn (touched, header, _, entries, result) =>
- (touched, header, make_perspective ids, entries, result));
+ map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
val visible_command = #1 o get_perspective;
val visible_last = #2 o get_perspective;
val visible_node = is_some o visible_last
fun map_entries f =
- map_node (fn (touched, header, perspective, entries, result) =>
- (touched, header, perspective, f entries, result));
+ map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
fun get_entries (Node {entries, ...}) = entries;
fun iterate_entries f = Entries.iterate NONE f o get_entries;
@@ -126,8 +115,7 @@
fun get_result (Node {result, ...}) = result;
fun set_result result =
- map_node (fn (touched, header, perspective, entries, _) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
fun default_node name = Graph.default_node (name, empty_node);
@@ -182,30 +170,13 @@
fun nodes_of (Version nodes) = nodes;
val node_of = get_node o nodes_of;
-local
-
fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
-fun touch_node name nodes =
- fold (fn desc =>
- update_node desc
- (set_touched true #>
- desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec)))
- (Graph.all_succs nodes [name]) nodes;
-
-in
-
fun edit_nodes (name, node_edit) (Version nodes) =
Version
(case node_edit of
- Clear =>
- nodes
- |> update_node name clear_node
- |> touch_node name
- | Edits edits =>
- nodes
- |> update_node name (edit_node edits)
- |> touch_node name
+ Clear => update_node name clear_node nodes
+ | Edits edits => update_node name (edit_node edits) nodes
| Header header =>
let
val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
@@ -222,11 +193,7 @@
(header', Graph.add_deps_acyclic (name, imports) nodes2)
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
in Graph.map_node name (set_header header'') nodes3 end
- |> touch_node name
- | Perspective perspective =>
- update_node name (set_perspective perspective #> set_touched true) nodes);
-
-end;
+ | Perspective perspective => update_node name (set_perspective perspective) nodes);
fun put_node (name, node) (Version nodes) =
Version (update_node name (K node) nodes);
@@ -388,7 +355,7 @@
Symtab.update (a, ())) all_visible Symtab.empty;
in Symtab.defined required end;
-fun init_theory deps node =
+fun init_theory imports node =
let
(* FIXME provide files via Scala layer, not master_dir *)
val (dir, header) = Exn.release (get_header node);
@@ -402,8 +369,8 @@
SOME thy => thy
| NONE =>
Toplevel.end_theory (Position.file_only import)
- (fst (Command.memo_eval (* FIXME memo_result !?! *)
- (get_result (snd (Future.join (the (AList.lookup (op =) deps import)))))))));
+ (fst (Command.memo_result
+ (get_result (snd (the (AList.lookup (op =) imports import))))))));
in Thy_Load.begin_theory master_dir header parents end;
fun check_theory nodes name =
@@ -460,9 +427,9 @@
#1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
|> modify_init
|> Toplevel.put_id exec_id'_string);
- val exec' = Command.memo (fn () =>
- let val (st, _) = Command.memo_eval (snd (snd command_exec)); (* FIXME memo_result !?! *)
- in Command.run_command (tr ()) st end);
+ val exec' =
+ Command.memo (fn () =>
+ Command.run_command (tr ()) (fst (Command.memo_result (snd (snd command_exec)))));
val command_exec' = (command_id', (exec_id', exec'));
in SOME (command_exec' :: execs, command_exec', init') end;
@@ -481,21 +448,28 @@
val updated =
nodes |> Graph.schedule
(fn deps => fn (name, node) =>
- if is_touched node orelse is_required name andalso not (stable_finished_theory node) then
- let
- val node0 = node_of old_version name;
- fun init () = init_theory deps node;
- val bad_init =
- not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
- in
- (singleton o Future.forks)
- {name = "Document.update", group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
- (fn () =>
+ (singleton o Future.forks)
+ {name = "Document.update", group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
+ (fn () =>
+ let
+ val imports = map (apsnd Future.join) deps;
+ val updated_imports = exists (is_some o #3 o #1 o #2) imports;
+ val required = is_required name;
+ in
+ if updated_imports orelse AList.defined (op =) edits name orelse
+ required andalso not (stable_finished_theory node)
+ then
let
- val required = is_required name;
+ val node0 = node_of old_version name;
+ fun init () = init_theory imports node;
+ val bad_init =
+ not (check_theory nodes name andalso forall (check_theory nodes o #1) imports);
+
val last_visible = visible_last node;
- val (common, (visible, initial)) = last_common state last_visible node0 node;
+ val (common, (visible, initial)) =
+ if updated_imports then (NONE, (true, true))
+ else last_common state last_visible node0 node;
val common_command_exec = the_default_entry node common;
val (new_execs, (command_id', (_, exec')), _) =
@@ -521,17 +495,19 @@
val node' = node
|> fold reset_entry no_execs
|> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
- |> set_result result
- |> set_touched false;
- in ((no_execs, new_execs, [(name, node')]), node') end)
- end
- else Future.value (([], [], []), node))
+ |> set_result result;
+ val updated_node =
+ if null no_execs andalso null new_execs then NONE
+ else SOME (name, node');
+ in ((no_execs, new_execs, updated_node), node') end
+ else (([], [], NONE), node)
+ end))
|> Future.joins |> map #1;
val command_execs =
map (rpair NONE) (maps #1 updated) @
map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
- val updated_nodes = maps #3 updated;
+ val updated_nodes = map_filter #3 updated;
val state' = state
|> define_version new_id (fold put_node updated_nodes new_version);