# HG changeset patch
# User wenzelm
# Date 1506511792 -7200
# Node ID 16fd7655d39d14c10be945a17c0de974ac3158f0
# Parent  5b9dc3f7bcde7082a87ab48c438735d6219ae23f
slightly more parallelism;

diff -r 5b9dc3f7bcde -r 16fd7655d39d src/Pure/PIDE/resources.scala
--- 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)