maintain loaded_files for each theory;

--- a/src/Pure/PIDE/resources.scala	Wed Sep 27 14:48:25 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 17:39:03 2017 +0200
@@ -72,19 +72,18 @@
     }
   }
 
-  def pure_files(syntax: Outer_Syntax, session: String, dir: Path): List[Path] =
-    if (Sessions.is_pure(session)) {
-      val roots =
-        for { (name, _) <- Thy_Header.ml_roots }
-        yield (dir + Path.explode(name)).expand
-      val files =
-        for {
-          (path, (_, theory)) <- roots zip Thy_Header.ml_roots
-          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
-        } yield file
-      roots ::: files
-    }
-    else Nil
+  def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] =
+  {
+    val roots =
+      for { (name, _) <- Thy_Header.ml_roots }
+      yield (dir + Path.explode(name)).expand
+    val files =
+      for {
+        (path, (_, theory)) <- roots zip Thy_Header.ml_roots
+        file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
+      } yield file
+    roots ::: files
+  }
 
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))

--- a/src/Pure/Thy/sessions.scala	Wed Sep 27 14:48:25 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Sep 27 17:39:03 2017 +0200
@@ -27,7 +27,9 @@
   {
     val empty: Known = Known()
 
-    def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
+    def make(local_dir: Path, bases: List[Base],
+      theories: List[Document.Node.Name] = Nil,
+      loaded_files: List[(String, List[Path])] = Nil): Known =
     {
       def bases_iterator(local: Boolean) =
         for {
@@ -66,15 +68,21 @@
               known
             else known + (file -> (name :: theories1))
         })
+
+      val known_loaded_files =
+        (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
+
       Known(known_theories, known_theories_local,
-        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
+        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
+        known_loaded_files)
     }
   }
 
   sealed case class Known(
     theories: Map[String, Document.Node.Name] = Map.empty,
     theories_local: Map[String, Document.Node.Name] = Map.empty,
-    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
+    files: Map[JFile, List[Document.Node.Name]] = Map.empty,
+    loaded_files: Map[String, List[Path]] = Map.empty)
   {
     def platform_path: Known =
       copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
@@ -174,7 +182,7 @@
               }
             val imports_base: Sessions.Base =
               parent_base.copy(known =
-                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
+                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
 
             val resources = new Resources(imports_base)
 
@@ -200,12 +208,16 @@
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files =
               if (inlined_files) {
-                resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files
+                if (Sessions.is_pure(info.name)) {
+                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
+                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
+                }
+                else thy_deps.loaded_files
               }
               else Nil
 
             val all_files =
-              (theory_files ::: loaded_files :::
+              (theory_files ::: loaded_files.flatMap(_._2) :::
                 info.files.map(file => info.dir + file) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
@@ -248,6 +260,11 @@
                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
             }
 
+            val known =
+              Known.make(info.dir, List(imports_base),
+                theories = thy_deps.deps.map(_.name),
+                loaded_files = loaded_files)
+
             val sources =
               for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
             val sources_errors =
@@ -258,7 +275,7 @@
                 pos = info.pos,
                 global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
-                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
+                known = known,
                 keywords = thy_deps.keywords,
                 syntax = syntax,
                 sources = sources,
@@ -275,13 +292,14 @@
           }
       })
 
-    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
+    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
   }
 
   def session_base_errors(
     options: Options,
     session: String,
     dirs: List[Path] = Nil,
+    inlined_files: Boolean = false,
     all_known: Boolean = false): (List[String], Base) =
   {
     val full_sessions = load(options, dirs = dirs)
@@ -289,7 +307,8 @@
     val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
 
     val sessions: T = if (all_known) full_sessions else selected_sessions
-    val deps = Sessions.deps(sessions, global_theories = global_theories)
+    val deps =
+      Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories)
     val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
     (deps.errors, base)
   }
@@ -298,9 +317,12 @@
     options: Options,
     session: String,
     dirs: List[Path] = Nil,
+    inlined_files: Boolean = false,
     all_known: Boolean = false): Base =
   {
-    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
+    val (errs, base) =
+      session_base_errors(options, session, dirs = dirs,
+        inlined_files = inlined_files, all_known = all_known)
     if (errs.isEmpty) base else error(cat_lines(errs))
   }
 

--- a/src/Pure/Thy/thy_info.scala	Wed Sep 27 14:48:25 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Sep 27 17:39:03 2017 +0200
@@ -88,11 +88,11 @@
             (name.theory_base_name -> name.theory)  // legacy
       }
 
-    def loaded_files: List[Path] =
+    def loaded_files: List[(String, List[Path])] =
     {
-      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 }
+      val names = deps.map(_.name)
+      names.map(_.theory) zip
+        Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
     }
 
     override def toString: String = deps.toString