# HG changeset patch
# User wenzelm
# Date 1546283616 -3600
# Node ID 195371990820547ab55ecd8d14e91ffbd3140983
# Parent  66c8dff9639f580277fefe5333cb71d2c0303581
clarified signature;

diff -r 66c8dff9639f -r 195371990820 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Dec 31 20:08:32 2018 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Dec 31 20:13:36 2018 +0100
@@ -90,11 +90,12 @@
     }
   }
 
-  def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] =
+  def pure_files(syntax: Outer_Syntax): List[Path] =
   {
+    val pure_dir = Path.explode("~~/src/Pure")
     val roots =
       for { (name, _) <- Thy_Header.ml_roots }
-      yield (dir + Path.explode(name)).expand
+      yield (pure_dir + Path.explode(name)).expand
     val files =
       for {
         (path, (_, theory)) <- roots zip Thy_Header.ml_roots
@@ -344,11 +345,20 @@
         graph2.map_node(name, _ => syntax)
       })
 
-    def loaded_files: List[(String, List[Path])] =
+    def loaded_files(is_pure: Boolean): List[(String, List[Path])] =
     {
-      theories.map(_.theory) zip
-        Par_List.map((e: () => List[Path]) => e(),
-          theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+      val loaded_files =
+        theories.map(_.theory) zip
+          Par_List.map((e: () => List[Path]) => e(),
+            theories.map(name =>
+              resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+
+      if (is_pure) {
+        val pure_files = resources.pure_files(overall_syntax)
+        loaded_files.map({ case (name, files) =>
+          (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
+      }
+      else loaded_files
     }
 
     def imported_files: List[Path] =
diff -r 66c8dff9639f -r 195371990820 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 31 20:08:32 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 31 20:13:36 2018 +0100
@@ -303,14 +303,7 @@
 
             val theory_files = dependencies.theories.map(_.path)
             val loaded_files =
-              if (inlined_files) {
-                if (Sessions.is_pure(info.name)) {
-                  val pure_files = resources.pure_files(overall_syntax, info.dir)
-                  dependencies.loaded_files.map({ case (name, files) =>
-                    (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
-                }
-                else dependencies.loaded_files
-              }
+              if (inlined_files) dependencies.loaded_files(Sessions.is_pure(info.name))
               else Nil
 
             val session_files =