src/Pure/PIDE/document.ML
changeset 44223 cac52579f2c2
parent 44222 9d5ef6cd4ee1
child 44226 1ea760da0f2d
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 16 21:13:52 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 16 21:50:53 2011 +0200
     1.3 @@ -86,7 +86,6 @@
     1.4  val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
     1.5  
     1.6  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
     1.7 -fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
     1.8  fun default_node name = Graph.default_node (name, empty_node);
     1.9  fun update_node name f = default_node name #> Graph.map_node name f;
    1.10  
    1.11 @@ -141,10 +140,12 @@
    1.12            |> update_node name (edit_node edits)
    1.13        | Header header =>
    1.14            let
    1.15 -            val node = get_node nodes name;
    1.16 -            val nodes1 = Graph.new_node (name, node) (remove_node name nodes);
    1.17              val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
    1.18 -            val nodes2 = fold default_node parents nodes1;
    1.19 +            val nodes1 = nodes
    1.20 +              |> default_node name
    1.21 +              |> fold default_node parents;
    1.22 +            val nodes2 = nodes1
    1.23 +              |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.24              val (header', nodes3) =
    1.25                (header, Graph.add_deps_acyclic (name, parents) nodes2)
    1.26                  handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);