--- 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
--- 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) {