src/Pure/PIDE/document.scala
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