# HG changeset patch
# User wenzelm
# Date 1676810618 -3600
# Node ID 57467fdd507d4605068a2522ef83358edcb514ab
# Parent  026e1bb04a051b4f652d9bf9d4511f3d579b9c6d
unused;

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