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 }