unused;

--- 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
     }