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