# HG changeset patch
# User wenzelm
# Date 1671302149 -3600
# Node ID 254964ca1b9844f593c37c8ff10943ca39889dc2
# Parent  b04d45bebbc59c510dcdfeba19c1a4400f46a773
clarified signature: avoid case class with redefined equality;

diff -r b04d45bebbc5 -r 254964ca1b98 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 17 19:19:10 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 17 19:35:49 2022 +0100
@@ -91,6 +91,9 @@
     def bad_header(msg: String): Header = Header(errors = List(msg))
 
     object Name {
+      def apply(node: String, master_dir: String = "", theory: String = ""): Name =
+        new Name(node, master_dir, theory)
+
       val empty: Name = Name("")
 
       object Ordering extends scala.math.Ordering[Name] {
@@ -103,7 +106,7 @@
         Graph.make(entries, symmetric = true)(Ordering)
     }
 
-    sealed case class Name(node: String, master_dir: String = "", theory: String = "") {
+    final class Name private(val node: String, val master_dir: String, val theory: String) {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
         that match {
@@ -123,8 +126,8 @@
 
       override def toString: String = if (is_theory) theory else node
 
-      def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
-      def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
+      def map(f: String => String): Name =
+        new Name(f(node), f(master_dir), theory)
 
       def json: JSON.Object.T =
         JSON.Object("node_name" -> node, "theory_name" -> theory)