changeset 70676 | 73812c598a26 |
parent 70674 | 29bb1ebb188f |
child 70692 | 41b5e515c238 |
--- a/src/Pure/PIDE/document.scala Sun Sep 08 16:49:05 2019 +0200 +++ b/src/Pure/PIDE/document.scala Sun Sep 08 16:49:32 2019 +0200 @@ -126,6 +126,7 @@ } def path: Path = Path.explode(File.standard_path(node)) + def master_dir_path: Path = Path.explode(File.standard_path(master_dir)) def is_theory: Boolean = theory.nonEmpty