# HG changeset patch
# User wenzelm
# Date 1672486500 -3600
# Node ID 252ed80e1a567a7ce88f0b68b692cceae3537f50
# Parent  83e3d4075f2c59ec66dabf11f720053295cba562
unused;

diff -r 83e3d4075f2c -r 252ed80e1a56 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 31 12:31:31 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 31 12:35:00 2022 +0100
@@ -128,16 +128,11 @@
 
       override def toString: String = if (is_theory) theory else node
 
-      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)
     }
 
     sealed case class Entry(name: Node.Name, header: Node.Header) {
-      def map(f: String => String): Entry = copy(name = name.map(f))
-
       override def toString: String = name.toString
     }