--- a/src/Pure/PIDE/document.scala Sun Feb 19 13:43:38 2023 +0100
+++ b/src/Pure/PIDE/document.scala Sun Feb 19 13:47:10 2023 +0100
@@ -416,7 +416,8 @@
if name == file_name
} yield cmd).toList
- def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
+ def descendants(names: List[Node.Name]): List[Node.Name] =
+ names.foldLeft(graph)(Nodes.init).all_succs(names)
def topological_order: List[Node.Name] = graph.topological_order
override def toString: String = topological_order.mkString("Nodes(", ",", ")")