# HG changeset patch
# User wenzelm
# Date 1676810830 -3600
# Node ID c6d7246926036dfcffadd813c5b1513862d9d0df
# Parent  57467fdd507d4605068a2522ef83358edcb514ab
proper Nodes.init (amending 9b35c1171d9a);

diff -r 57467fdd507d -r c6d724692603 src/Pure/PIDE/document.scala
--- 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(", ",", ")")