# HG changeset patch
# User wenzelm
# Date 1567762358 -7200
# Node ID 4655897b828724a9f3296b31d48bc2d7237457dd
# Parent  2bf1d0e576954a8b195a2f34c09251ea3404523b
unused;

diff -r 2bf1d0e57695 -r 4655897b8287 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