tuned signature;

--- a/src/Pure/PIDE/resources.scala	Tue Jul 21 12:37:00 2020 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Jul 21 19:40:38 2020 +0200
@@ -342,7 +342,7 @@
     def entries: List[Document.Node.Entry] = rev_entries.reverse
 
     def theories: List[Document.Node.Name] = entries.map(_.name)
-    def adjunct_theories: List[(A, Document.Node.Name)] = theories.map(name => (seen(name), name))
+    def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name)))
 
     def errors: List[String] = entries.flatMap(_.header.errors)
 

--- a/src/Pure/Thy/sessions.scala	Tue Jul 21 12:37:00 2020 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Jul 21 19:40:38 2020 +0200
@@ -249,22 +249,15 @@
 
             val known_loaded_files = imports_base.known_loaded_files ++ loaded_files
 
-            val used_theories =
-              for ((options, name) <- dependencies.adjunct_theories)
-              yield (name, options)
-
-            def used_theories_session_iterator: Iterator[Document.Node.Name] =
-              for {
-                (name, _) <- used_theories.iterator
-                if imports_base.theory_qualifier(name) == session_name
-              } yield name
+            val used_theories_session =
+              dependencies.theories.filter(name => imports_base.theory_qualifier(name) == session_name)
 
             val dir_errors =
             {
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
-                  name <- used_theories_session_iterator
+                  name <- used_theories_session.iterator
                   path = name.master_dir_path
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
@@ -280,7 +273,7 @@
               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
               val errs4 =
                 (for {
-                  name <- used_theories_session_iterator
+                  name <- used_theories_session.iterator
                   name1 <- resources.find_theory_node(name.theory)
                   if name.node != name1.node
                 } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
@@ -307,7 +300,7 @@
                 session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
                 loaded_theories = dependencies.loaded_theories,
-                used_theories = used_theories,
+                used_theories = dependencies.theories_adjunct,
                 known_theories = known_theories,
                 known_loaded_files = known_loaded_files,
                 overall_syntax = overall_syntax,