# HG changeset patch
# User wenzelm
# Date 1506504590 -7200
# Node ID 5b9dc3f7bcde7082a87ab48c438735d6219ae23f
# Parent  190834aa43a7b21fec599668fd358b92aa9f1a29
prefer sequential file-system access, but parallel parse;

diff -r 190834aa43a7 -r 5b9dc3f7bcde src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Sep 27 11:11:07 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 11:29:50 2017 +0200
@@ -57,16 +57,18 @@
 
   /* theory files */
 
-  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): List[Path] =
+  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
   {
     val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
-    if (syntax.load_commands_in(text)) {
-      val spans = syntax.parse_spans(text)
-      val dir = Path.explode(name.master_dir)
-      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
-        map(a => dir + Path.explode(a)).toList
+    () => {
+      if (syntax.load_commands_in(text)) {
+        val spans = syntax.parse_spans(text)
+        val dir = Path.explode(name.master_dir)
+        spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
+          map(a => dir + Path.explode(a)).toList
+      }
+      else Nil
     }
-    else Nil
   }
 
   def pure_files(syntax: Outer_Syntax, session: String, dir: Path): List[Path] =
@@ -77,7 +79,7 @@
       val files =
         for {
           (path, (_, theory)) <- roots zip Thy_Header.ml_roots
-          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))
+          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
         } yield file
       roots ::: files
     }
diff -r 190834aa43a7 -r 5b9dc3f7bcde src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Wed Sep 27 11:11:07 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Sep 27 11:29:50 2017 +0200
@@ -90,8 +90,8 @@
 
     def loaded_files: List[Path] =
     {
-      val dep_files =
-        Par_List.map((dep: Thy_Info.Dep) => resources.loaded_files(syntax, dep.name), rev_deps)
+      val parses = rev_deps.map(dep => resources.loaded_files(syntax, dep.name))
+      val dep_files = Par_List.map((parse: () => List[Path]) => parse(), parses)
       ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     }