# HG changeset patch
# User wenzelm
# Date 1672483712 -3600
# Node ID 893eeef9ef08a2052d2a70a74ebd9b3cc52ea1a0
# Parent  2121fde115b2435df5fdace356ddeb45256eb497
clarified signature;

diff -r 2121fde115b2 -r 893eeef9ef08 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sat Dec 31 11:35:28 2022 +0100
+++ b/src/Pure/General/graph.scala	Sat Dec 31 11:48:32 2022 +0100
@@ -27,7 +27,7 @@
 
   def make[Key, A](
     entries: List[((Key, A), List[Key])],
-    symmetric: Boolean = false)(
+    converse: Boolean = false)(
     implicit ord: Ordering[Key]
   ): Graph[Key, A] = {
     val graph1 =
@@ -38,7 +38,7 @@
       entries.foldLeft(graph1) {
         case (graph, ((x, _), ys)) =>
           ys.foldLeft(graph) {
-            case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y)
+            case (g, y) => if (converse) g.add_edge(y, x) else g.add_edge(x, y)
           }
       }
     graph2
diff -r 2121fde115b2 -r 893eeef9ef08 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 31 11:35:28 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 31 11:48:32 2022 +0100
@@ -103,7 +103,7 @@
       type Graph[A] = isabelle.Graph[Node.Name, A]
 
       def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] =
-        Graph.make(entries, symmetric = true)(Ordering)
+        Graph.make(entries, converse = true)(Ordering)
     }
 
     final class Name private(val node: String, val master_dir: String, val theory: String) {