# HG changeset patch
# User wenzelm
# Date 1572630112 -3600
# Node ID d8a7df9fdd03d2ef13389aa822586a38a5d5b9ec
# Parent  2866fee241eecc21e9a9f70f1e9856937f469e44
more operations;

diff -r 2866fee241ee -r d8a7df9fdd03 src/Pure/PIDE/document.scala
--- 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(", ",", ")")