# HG changeset patch
# User wenzelm
# Date 1636154009 -3600
# Node ID eb89b3a378260f844f54dadb890f823f445a2c45
# Parent  2057c02d779519c2436a9a3365f3195d614426f2
proper used_theories for session build hierarchy, not known_theories from imported sessions;

diff -r 2057c02d7795 -r eb89b3a37826 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 23:38:59 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Nov 06 00:13:29 2021 +0100
@@ -429,10 +429,13 @@
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
-    val theory_exports0: Set[String] = html_context.cached_theories
+    val cached_theories: Set[String] = html_context.cached_theories
+    val all_used_theories = hierarchy.flatMap(a => deps(a).used_theories.map(_._1))
+    val present_theories = all_used_theories.filterNot(name => cached_theories.contains(name.theory))
+
     val theory_exports: Map[String, Export_Theory.Theory] =
-      (for ((_, entry) <- base.known_theories.iterator) yield {
-        val thy_name = entry.name.theory
+      (for (node <- all_used_theories.iterator) yield {
+        val thy_name = node.theory
         val theory =
           if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
           else {
@@ -562,10 +565,6 @@
         }
       }
 
-      val present_theories =
-        for ((name, _) <- base.used_theories if !theory_exports0.contains(name.theory))
-          yield name
-
       (for (thy <- Par_List.map(read_theory, present_theories).flatten) yield {
         val thy_session = base.theory_qualifier(thy.name)
         val thy_dir = make_session_dir(thy_session)