diff -r d924a69e7d2b -r 5786d6394659 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Jan 03 21:18:15 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Jan 03 21:22:04 2023 +0100
@@ -120,7 +120,6 @@
       def path: Path = Path.explode(File.standard_path(node))
 
       def master_dir: String = Url.strip_base_name(node).getOrElse("")
-      def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
 
       def is_theory: Boolean = theory.nonEmpty