# HG changeset patch
# User wenzelm
# Date 1506457854 -7200
# Node ID 8f863dae78a0ab093f8d7c9f1aa885b8f336016a
# Parent  91500c024c7f46e37a952c2bd417613d6647734b
clarified pure_files, based on uniform loaded_files;

diff -r 91500c024c7f -r 8f863dae78a0 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Sep 26 20:54:40 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Sep 26 22:30:54 2017 +0200
@@ -57,20 +57,32 @@
 
   /* theory files */
 
-  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
-    if (syntax.load_commands_in(text)) {
-      val spans = syntax.parse_spans(text)
-      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
-    }
-    else Nil
-
   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 dir = Path.explode(name.master_dir)
-    loaded_files(syntax, text).map(a => dir + Path.explode(a))
+    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
   }
 
+  def pure_files(syntax: Outer_Syntax, session: String, dir: Path): List[Path] =
+    if (Sessions.is_pure(session)) {
+      val roots =
+        for { (name, theory) <- Thy_Header.ml_roots }
+        yield ((dir + Path.explode(name)).expand, theory)
+      val files =
+        for {
+          (path, theory) <- roots
+          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))
+        } yield file
+      roots.map(_._1) ::: files
+    }
+    else Nil
+
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
diff -r 91500c024c7f -r 8f863dae78a0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Sep 26 20:54:40 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Sep 26 22:30:54 2017 +0200
@@ -200,16 +200,7 @@
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files =
               if (inlined_files) {
-                val pure_files =
-                  if (is_pure(info.name)) {
-                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
-                    val files =
-                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
-                        map(file => info.dir + Path.explode(file))
-                    roots ::: files
-                  }
-                  else Nil
-                pure_files ::: thy_deps.loaded_files
+                resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files
               }
               else Nil