# HG changeset patch
# User wenzelm
# Date 1636138415 -3600
# Node ID 9d7f95c43584b7b8897ff3393b24a5d270ec5c87
# Parent  531bb10a288ccac209891bed29c00a23972252d4
observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid;

diff -r 531bb10a288c -r 9d7f95c43584 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 19:15:18 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 05 19:53:35 2021 +0100
@@ -389,6 +389,7 @@
     elements: Elements,
     presentation: Context): Unit =
   {
+    val hierarchy = deps.sessions_structure.hierarchy(session)
     val info = deps.sessions_structure(session)
     val options = info.options
     val base = deps(session)
@@ -438,16 +439,9 @@
           else {
             html_context.cache_theory(thy_name,
               {
-                val qualifier = deps(session).theory_qualifier(thy_name)
                 val provider =
-                  Export.Provider.database_context(db_context, List(qualifier), thy_name)
-                if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
-                  Export_Theory.read_theory(provider, qualifier, thy_name)
-                }
-                else {
-                  progress.echo_warning("No theory exports for " + quote(thy_name))
-                  Export_Theory.no_theory
-                }
+                  Export.Provider.database_context(db_context, hierarchy, thy_name)
+                Export_Theory.read_theory(provider, session, thy_name)
               })
         }
         thy_name -> theory