--- a/src/Pure/PIDE/resources.scala Fri Nov 27 11:50:23 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Nov 27 14:00:54 2020 +0100
@@ -117,8 +117,10 @@
val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
val spans = syntax.parse_spans(text)
val dir = Path.explode(name.master_dir)
- spans.iterator.flatMap(Command.span_files(syntax, _)._1).
- map(a => (dir + Path.explode(a)).expand).toList
+ (for {
+ span <- spans.iterator
+ file <- span.loaded_files(syntax)._1
+ } yield (dir + Path.explode(file)).expand).toList
}
else Nil
}