unused;
authorwenzelm
Fri, 06 Sep 2019 11:32:38 +0200
changeset 70848 4655897b8287
parent 70847 2bf1d0e57695
child 70849 44588e355ca8
unused;
src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Fri Sep 06 11:32:24 2019 +0200
+++ b/src/Pure/PIDE/document_status.scala	Fri Sep 06 11:32:38 2019 +0200
@@ -244,12 +244,6 @@
         node_status <- get(name)
       } yield (name, node_status)).toList
 
-    def consolidated(name: Document.Node.Name): Boolean =
-      rep.get(name) match {
-        case Some(st) => st.consolidated
-        case None => false
-      }
-
     def quasi_consolidated(name: Document.Node.Name): Boolean =
       rep.get(name) match {
         case Some(st) => st.quasi_consolidated