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