src/Pure/PIDE/document_status.scala

     val empty: Nodes_Status = new Nodes_Status(Map.empty)
   }
 
   final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
   {
-    def keys_iterator: Iterator[Document.Node.Name] = rep.keysIterator
-
     def defined(name: Document.Node.Name): Boolean = rep.isDefinedAt(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
     def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
       rep.get(name) match {

       }
 
     def + (entry: (Document.Node.Name, Node_Status)): Nodes_Status =
       new Nodes_Status(rep + entry)
 
-    def - (name: Document.Node.Name): Nodes_Status =
-      new Nodes_Status(rep - name)
-
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Nodes_Status => rep == other.rep
         case _ => false