# HG changeset patch
# User wenzelm
# Date 1636037077 -3600
# Node ID 7e31f7022c7b40d1df929fd5c53b8c6505ca0865
# Parent  4a45dfee3402cd08ffbc23e7becc24c851151036
clarified signature;

diff -r 4a45dfee3402 -r 7e31f7022c7b src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu Nov 04 12:53:12 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Thu Nov 04 15:44:37 2021 +0100
@@ -116,19 +116,21 @@
         (for ((k, xs) <- others.iterator) yield cache.string(k) -> xs.map(_.cache(cache))).toMap)
   }
 
+  def read_theory_parents(provider: Export.Provider, theory_name: String): Option[List[String]] =
+  {
+    if (theory_name == Thy_Header.PURE) Some(Nil)
+    else {
+      provider(Export.THEORY_PREFIX + "parents")
+        .map(entry => split_lines(entry.uncompressed.text))
+    }
+  }
+
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
     cache: Term.Cache = Term.Cache.none): Theory =
   {
     val parents =
-      if (theory_name == Thy_Header.PURE) Nil
-      else {
-        provider(Export.THEORY_PREFIX + "parents") match {
-          case Some(entry) => split_lines(entry.uncompressed.text)
-          case None =>
-            error("Missing theory export in session " + quote(session_name) + ": " +
-              quote(theory_name))
-        }
-      }
+      read_theory_parents(provider, theory_name) getOrElse
+        error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name))
     val theory =
       Theory(theory_name, parents,
         read_types(provider),
diff -r 4a45dfee3402 -r 7e31f7022c7b src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 04 12:53:12 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 04 15:44:37 2021 +0100
@@ -439,13 +439,13 @@
         else {
           val session1 = deps(session).theory_qualifier(name)
           val provider = Export.Provider.database_context(db_context, List(session1), name.theory)
-          provider(Export.THEORY_PREFIX + "parents") match {
-            case Some(_) =>
-              val theory = Export_Theory.read_theory(provider, session1, name.theory)
-              theory.entity_iterator.toVector
-            case None =>
-              progress.echo_warning("No theory exports for " + name)
-              Vector.empty
+          if (Export_Theory.read_theory_parents(provider, name.theory).isDefined) {
+            val theory = Export_Theory.read_theory(provider, session1, name.theory)
+            theory.entity_iterator.toVector
+          }
+          else {
+            progress.echo_warning("No theory exports for " + name)
+            Vector.empty
           }
         }
       })