discontinued fragile operation;
authorwenzelm
Tue, 03 Jan 2023 21:22:04 +0100
changeset 76891 5786d6394659
parent 76890 d924a69e7d2b
child 76892 7fd3e461d3b6
discontinued fragile operation;
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