# HG changeset patch
# User wenzelm
# Date 1659524852 -7200
# Node ID 8dc9d979bbacb50264c5fa90cd91065e40014a32
# Parent  3513fdfeb4d8da3a5ff207961fb2d8cea1decf18
clarified signature;

diff -r 3513fdfeb4d8 -r 8dc9d979bbac src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Aug 03 12:58:17 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Wed Aug 03 13:07:32 2022 +0200
@@ -122,29 +122,33 @@
     provider: Export.Provider,
     session_name: String,
     theory_name: String,
+    permissive: Boolean = false,
     cache: Term.Cache = Term.Cache.none
   ): Theory = {
     val theory_provider = provider.focus(theory_name)
-    val parents =
-      read_theory_parents(theory_provider, theory_name) getOrElse
+    read_theory_parents(theory_provider, theory_name) match {
+      case None if permissive => no_theory
+      case None =>
         error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name))
-    val theory =
-      Theory(theory_name, parents,
-        read_types(theory_provider),
-        read_consts(theory_provider),
-        read_axioms(theory_provider),
-        read_thms(theory_provider),
-        read_classes(theory_provider),
-        read_locales(theory_provider),
-        read_locale_dependencies(theory_provider),
-        read_classrel(theory_provider),
-        read_arities(theory_provider),
-        read_constdefs(theory_provider),
-        read_typedefs(theory_provider),
-        read_datatypes(theory_provider),
-        read_spec_rules(theory_provider),
-        read_others(theory_provider))
-    if (cache.no_cache) theory else theory.cache(cache)
+      case Some(parents) =>
+        val theory =
+          Theory(theory_name, parents,
+            read_types(theory_provider),
+            read_consts(theory_provider),
+            read_axioms(theory_provider),
+            read_thms(theory_provider),
+            read_classes(theory_provider),
+            read_locales(theory_provider),
+            read_locale_dependencies(theory_provider),
+            read_classrel(theory_provider),
+            read_arities(theory_provider),
+            read_constdefs(theory_provider),
+            read_typedefs(theory_provider),
+            read_datatypes(theory_provider),
+            read_spec_rules(theory_provider),
+            read_others(theory_provider))
+        if (cache.no_cache) theory else theory.cache(cache)
+    }
   }
 
   def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A = {
diff -r 3513fdfeb4d8 -r 8dc9d979bbac src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Aug 03 12:58:17 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Aug 03 13:07:32 2022 +0200
@@ -132,10 +132,8 @@
                     val theory =
                       if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
                       else {
-                        if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
-                          Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache)
-                        }
-                        else Export_Theory.no_theory
+                        Export_Theory.read_theory(provider, session, thy_name,
+                          permissive = true, cache = db_context.cache)
                       }
                     thy_name -> Node_Info.make(theory)
                   }