back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition";
authorwenzelm
Sat, 06 Nov 2021 18:16:54 +0100
changeset 74716 056de3681cb9
parent 74715 129fb11b357f
child 74717 baed95c97505
back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition";
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