author | wenzelm |
Sun, 19 Feb 2023 13:43:38 +0100 | |
changeset 77300 | 57467fdd507d |
parent 77299 | 026e1bb04a05 |
child 77301 | c6d724692603 |
--- a/src/Pure/PIDE/document.scala Sun Feb 19 13:37:38 2023 +0100 +++ b/src/Pure/PIDE/document.scala Sun Feb 19 13:43:38 2023 +0100 @@ -417,7 +417,6 @@ } 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_rev(names) def topological_order: List[Node.Name] = graph.topological_order override def toString: String = topological_order.mkString("Nodes(", ",", ")")