# HG changeset patch
# User wenzelm
# Date 1636219014 -3600
# Node ID 056de3681cb9da319f0899157d2cf7954b6a95c4
# Parent  129fb11b357fec75513dbc458f6c82ab44999dff
back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition";

diff -r 129fb11b357f -r 056de3681cb9 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Nov 06 15:25:20 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Nov 06 18:16:54 2021 +0100
@@ -443,8 +443,11 @@
             html_context.cache_theory(thy_name,
               {
                 val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
-                Export_Theory.read_theory(
-                  provider, session, thy_name, cache = html_context.term_cache)
+                if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
+                  Export_Theory.read_theory(
+                    provider, session, thy_name, cache = html_context.term_cache)
+                }
+                else Export_Theory.no_theory
               })
         }
         thy_name -> theory