changeset 70658 | 4655897b8287 |
parent 70653 | f7c5b30fc432 |
child 71601 | 97ccf48c2f0c |
--- 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