src/Pure/PIDE/document_status.scala

--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:40:23 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:52:12 2018 +0200
@@ -185,6 +185,9 @@
     def + (entry: (Document.Node.Name, Node_Status)): Nodes_Status =
       new Nodes_Status(rep + entry)
 
+    def restrict(domain: Set[Document.Node.Name]): Nodes_Status =
+      new Nodes_Status(rep -- rep.keysIterator.filterNot(domain))
+
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {