changeset 70986 | d8a7df9fdd03 |
parent 70780 | 034742453594 |
child 71601 | 97ccf48c2f0c |
--- 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(", ",", ")")