diff -r 72ac27ea12b2 -r 38e05b7ded61 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Nov 28 15:17:14 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Nov 28 15:53:46 2020 +0100 @@ -121,7 +121,7 @@ val dir = Path.explode(name.master_dir) (for { span <- spans.iterator - file <- span.loaded_files(syntax)._1 + file <- span.loaded_files(syntax).files } yield (dir + Path.explode(file)).expand).toList } else Nil