# HG changeset patch
# User wenzelm
# Date 1406119820 -7200
# Node ID 50ab1db5c0fdcb702cf91a6bbd0b1c324b473d06
# Parent  df1b3452d71cd2fa7f86fd1fa3cc54c462ddd7d7
avoid redundant data structure;

diff -r df1b3452d71c -r 50ab1db5c0fd src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Jul 23 13:01:30 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 23 14:50:20 2014 +0200
@@ -223,7 +223,13 @@
     | Perspective perspective => update_node name (set_perspective perspective) nodes);
 
 fun put_node (name, node) (Version nodes) =
-  Version (update_node name (K node) nodes);
+  let
+    val nodes1 = update_node name (K node) nodes;
+    val nodes2 =
+      if String_Graph.is_maximal nodes1 name andalso is_empty_node node
+      then String_Graph.del_node name nodes1
+      else nodes1;
+  in Version nodes2 end;
 
 end;
 
diff -r df1b3452d71c -r 50ab1db5c0fd src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jul 23 13:01:30 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 23 14:50:20 2014 +0200
@@ -293,9 +293,6 @@
 
   final class Nodes private(graph: Graph[Node.Name, Node])
   {
-    def get_name(s: String): Option[Node.Name] =
-      graph.keys_iterator.find(name => name.node == s)
-
     def apply(name: Node.Name): Node =
       graph.default_node(name, Node.empty).get_node(name)
 
@@ -307,7 +304,10 @@
         (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
       val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
-      new Nodes(graph3.map_node(name, _ => node))
+      new Nodes(
+        if (graph3.is_maximal(name) && node.is_empty) graph3.del_node(name)
+        else graph3.map_node(name, _ => node)
+      )
     }
 
     def iterator: Iterator[(Node.Name, Node)] =