1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 23 13:01:30 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 23 14:50:20 2014 +0200
     1.3 @@ -223,7 +223,13 @@
     1.4      | Perspective perspective => update_node name (set_perspective perspective) nodes);
     1.5  
     1.6  fun put_node (name, node) (Version nodes) =
     1.7 -  Version (update_node name (K node) nodes);
     1.8 +  let
     1.9 +    val nodes1 = update_node name (K node) nodes;
    1.10 +    val nodes2 =
    1.11 +      if String_Graph.is_maximal nodes1 name andalso is_empty_node node
    1.12 +      then String_Graph.del_node name nodes1
    1.13 +      else nodes1;
    1.14 +  in Version nodes2 end;
    1.15  
    1.16  end;
    1.17  

     2.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 13:01:30 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 14:50:20 2014 +0200
     2.3 @@ -293,9 +293,6 @@
     2.4  
     2.5    final class Nodes private(graph: Graph[Node.Name, Node])
     2.6    {
     2.7 -    def get_name(s: String): Option[Node.Name] =
     2.8 -      graph.keys_iterator.find(name => name.node == s)
     2.9 -
    2.10      def apply(name: Node.Name): Node =
    2.11        graph.default_node(name, Node.empty).get_node(name)
    2.12  
    2.13 @@ -307,7 +304,10 @@
    2.14          (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
    2.15        val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
    2.16        val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
    2.17 -      new Nodes(graph3.map_node(name, _ => node))
    2.18 +      new Nodes(
    2.19 +        if (graph3.is_maximal(name) && node.is_empty) graph3.del_node(name)
    2.20 +        else graph3.map_node(name, _ => node)
    2.21 +      )
    2.22      }
    2.23  
    2.24      def iterator: Iterator[(Node.Name, Node)] =