src/Pure/General/graph.scala
changeset 78235 aece9a063271
parent 76840 893eeef9ef08
--- a/src/Pure/General/graph.scala	Fri Jun 30 16:26:03 2023 +0200
+++ b/src/Pure/General/graph.scala	Sat Jul 01 16:27:34 2023 +0200
@@ -66,7 +66,16 @@
 }
 
 
-final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) {
+final class Graph[Key, A] private(
+  protected val rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]
+) {
+  override def hashCode: Int = rep.hashCode
+  override def equals(that: Any): Boolean =
+    that match {
+      case other: Graph[_, _] => rep == other.rep
+      case _ => false
+    }
+
   type Keys = SortedSet[Key]
   type Entry = (A, (Keys, Keys))