# HG changeset patch
# User wenzelm
# Date 1606503390 -3600
# Node ID 049a71febf056205ede904871e8d91caa091c2c0
# Parent  5a6f7212fc4d32f5273c4cee906754dd5b764f39
proper structural equality;

diff -r 5a6f7212fc4d -r 049a71febf05 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Fri Nov 27 16:44:36 2020 +0100
+++ b/src/Pure/General/path.scala	Fri Nov 27 19:56:30 2020 +0100
@@ -150,8 +150,15 @@
 }
 
 
-final class Path private(private val elems: List[Path.Elem]) // reversed elements
+final class Path private(protected val elems: List[Path.Elem]) // reversed elements
 {
+  override def hashCode: Int = elems.hashCode
+  override def equals(that: Any): Boolean =
+    that match {
+      case other: Path => elems == other.elems
+      case _ => false
+    }
+
   def is_current: Boolean = elems.isEmpty
   def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
   def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }