src/Pure/PIDE/resources.scala
changeset 72817 1c378ab75d48
parent 72816 ea4f86914cb2
child 72857 a9e091ccd450
--- a/src/Pure/PIDE/resources.scala	Sat Dec 05 12:14:40 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 05 12:43:21 2020 +0100
@@ -124,7 +124,7 @@
   def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span])
     : List[Path] =
   {
-    val dir = Path.explode(name.master_dir)
+    val dir = name.master_dir_path
     for { span <- spans; file <- span.loaded_files(syntax).files }
       yield (dir + Path.explode(file)).expand
   }