author | wenzelm |
Fri, 06 Sep 2019 11:32:38 +0200 (2019-09-06) | |
changeset 70658 | 4655897b8287 |
parent 70657 | 2bf1d0e57695 |
child 70659 | 44588e355ca8 |
--- 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