src/Pure/PIDE/document_status.scala

--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:33:40 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:40:23 2018 +0200
@@ -172,8 +172,6 @@
 
   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)
 
@@ -187,9 +185,6 @@
     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 {