slightly more parallelism;
authorwenzelm
Wed Sep 27 13:29:52 2017 +0200 (19 months ago)
changeset 6669916fd7655d39d
parent 66698 5b9dc3f7bcde
child 66700 5174ce7c84f0
slightly more parallelism;
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Sep 27 11:29:50 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 13:29:52 2017 +0200
     1.3 @@ -59,8 +59,9 @@
     1.4  
     1.5    def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
     1.6    {
     1.7 -    val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
     1.8 +    val raw_text = with_thy_reader(name, reader => reader.source.toString)
     1.9      () => {
    1.10 +      val text = Symbol.decode(raw_text)
    1.11        if (syntax.load_commands_in(text)) {
    1.12          val spans = syntax.parse_spans(text)
    1.13          val dir = Path.explode(name.master_dir)