changeset 68904 | 09151c54aaac |
parent 68903 | 58525b08eed1 |
child 69255 | 800b1ce96fce |
--- a/src/Pure/PIDE/document_status.scala Tue Sep 04 14:40:31 2018 +0200 +++ b/src/Pure/PIDE/document_status.scala Tue Sep 04 14:47:50 2018 +0200 @@ -230,7 +230,7 @@ def apply(name: Document.Node.Name): Node_Status = rep(name) def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name) - def dest: List[(Document.Node.Name, Node_Status)] = + def present: List[(Document.Node.Name, Node_Status)] = for { name <- nodes.topological_order; node_status <- get(name) } yield (name, node_status)