slightly more parallelism;
authorwenzelm
Wed, 27 Sep 2017 13:29:52 +0200
changeset 66699 16fd7655d39d
parent 66698 5b9dc3f7bcde
child 66700 5174ce7c84f0
slightly more parallelism;
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)