--- a/src/Pure/PIDE/resources.scala Wed Sep 27 11:29:50 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Wed Sep 27 13:29:52 2017 +0200
@@ -59,8 +59,9 @@
def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
{
- val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
+ val raw_text = with_thy_reader(name, reader => reader.source.toString)
() => {
+ val text = Symbol.decode(raw_text)
if (syntax.load_commands_in(text)) {
val spans = syntax.parse_spans(text)
val dir = Path.explode(name.master_dir)