src/Pure/PIDE/document.scala

       val graph1 = Nodes.init(graph, name)
       graph1.is_maximal(name) && graph1.get_node(name).is_empty
     }
 
     def purge_suppressed: Option[Nodes] =
-      graph.keys_iterator.filter(suppressed).toList match {
+      names_iterator.filter(suppressed).toList match {
         case Nil => None
         case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_))))
       }
 
     def + (entry: (Node.Name, Node)): Nodes = {

     def domain: Set[Node.Name] = graph.domain
 
     def iterator: Iterator[(Node.Name, Node)] =
       graph.iterator.map({ case (name, (node, _)) => (name, node) })
 
+    def names_iterator: Iterator[Node.Name] = graph.keys_iterator
+
     def theory_name(theory: String): Option[Node.Name] =
-      graph.keys_iterator.find(name => name.theory == theory)
+      names_iterator.find(name => name.theory == theory)
 
     def commands_loading(file_name: Node.Name): List[Command] =
       (for {
         (_, node) <- iterator
         cmd <- node.load_commands.iterator