src/Pure/PIDE/resources.scala

--- a/src/Pure/PIDE/resources.scala	Thu Dec 22 08:56:16 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 22 15:23:26 2022 +0100
@@ -70,6 +70,8 @@
 
   /* file-system operations */
 
+  def migrate_name(name: Document.Node.Name): Document.Node.Name = name
+
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode