# HG changeset patch
# User wenzelm
# Date 1313524253 -7200
# Node ID cac52579f2c2d7d90fb49ec94732a23233011613
# Parent  9d5ef6cd4ee16fc33477f358100b764463a466d4
more robust treatment of node dependencies in incremental edits;

diff -r 9d5ef6cd4ee1 -r cac52579f2c2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 16 21:13:52 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 16 21:50:53 2011 +0200
@@ -86,7 +86,6 @@
 val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
 
 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
-fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
 fun default_node name = Graph.default_node (name, empty_node);
 fun update_node name f = default_node name #> Graph.map_node name f;
 
@@ -141,10 +140,12 @@
           |> update_node name (edit_node edits)
       | Header header =>
           let
-            val node = get_node nodes name;
-            val nodes1 = Graph.new_node (name, node) (remove_node name nodes);
             val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
-            val nodes2 = fold default_node parents nodes1;
+            val nodes1 = nodes
+              |> default_node name
+              |> fold default_node parents;
+            val nodes2 = nodes1
+              |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
             val (header', nodes3) =
               (header, Graph.add_deps_acyclic (name, parents) nodes2)
                 handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);