# 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