# HG changeset patch
# User wenzelm
# Date 1606835239 -3600
# Node ID 5dc7165e8a26653b55c9e2d03a9e185936432910
# Parent  402afc68f2f9ac645b9f556218d1f0a0f109cd1e
clarified signature;

diff -r 402afc68f2f9 -r 5dc7165e8a26 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/Pure/PIDE/headless.scala	Tue Dec 01 16:07:19 2020 +0100
@@ -256,7 +256,7 @@
       val dep_theories = dependencies.theories
       val dep_theories_set = dep_theories.toSet
       val dep_files =
-        dependencies.loaded_files(false).flatMap(_._2).
+        dependencies.loaded_files.flatMap(_._2).
           map(path => Document.Node.Name(resources.append("", path)))
 
       val use_theories_state =
diff -r 402afc68f2f9 -r 5dc7165e8a26 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/Pure/PIDE/resources.scala	Tue Dec 01 16:07:19 2020 +0100
@@ -398,20 +398,17 @@
         graph2.map_node(name, _ => syntax)
       })
 
-    def loaded_files(pure: Boolean): List[(String, List[Path])] =
+    def loaded_files: List[(String, List[Path])] =
     {
-      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 (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
+      theories.zip(
+        Par_List.map((e: () => List[Path]) => e(),
+          theories.map(name =>
+            resources.loaded_files(loaded_theories.get_node(name.theory), name))))
+        .map({ case (name, files) =>
+          val files1 =
+            if (name.theory == Thy_Header.PURE) resources.pure_files(overall_syntax) ::: files
+            else files
+          (name.theory, files1) })
     }
 
     def imported_files: List[Path] =
diff -r 402afc68f2f9 -r 5dc7165e8a26 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/Pure/Thy/sessions.scala	Tue Dec 01 16:07:19 2020 +0100
@@ -173,10 +173,7 @@
             val theory_files = dependencies.theories.map(_.path)
 
             val (loaded_files, loaded_files_errors) =
-              try {
-                if (inlined_files) (dependencies.loaded_files(Sessions.is_pure(info.name)), Nil)
-                else (Nil, Nil)
-              }
+              try { if (inlined_files) (dependencies.loaded_files, Nil) else (Nil, Nil) }
               catch { case ERROR(msg) => (Nil, List(msg)) }
 
             val session_files =