author | wenzelm |
Fri, 01 Nov 2019 18:41:52 +0100 | |
changeset 70986 | d8a7df9fdd03 |
parent 70985 | 2866fee241ee |
child 70987 | 6178ecf357a0 |
--- a/src/Pure/PIDE/document.scala Fri Nov 01 18:19:32 2019 +0100 +++ b/src/Pure/PIDE/document.scala Fri Nov 01 18:41:52 2019 +0100 @@ -408,6 +408,7 @@ } yield cmd).toList def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) + def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds(names).reverse def topological_order: List[Node.Name] = graph.topological_order override def toString: String = topological_order.mkString("Nodes(", ",", ")")