# HG changeset patch
# User wenzelm
# Date 1659524297 -7200
# Node ID 3513fdfeb4d8da3a5ff207961fb2d8cea1decf18
# Parent  ebbb7d6eb296d3fd90dab115441a48e914197f8f
clarified signature;

diff -r ebbb7d6eb296 -r 3513fdfeb4d8 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Wed Aug 03 12:25:37 2022 +0200
+++ b/src/Pure/Thy/export.scala	Wed Aug 03 12:58:17 2022 +0200
@@ -267,20 +267,20 @@
     def database(
       db: SQL.Database,
       cache: XML.Cache,
-      session_name: String,
-      theory_name: String
+      session: String,
+      theory: String = ""
     ) : Provider = {
       new Provider {
         def apply(export_name: String): Option[Entry] =
-          if (theory_name.isEmpty) None
+          if (theory.isEmpty) None
           else {
-            Entry_Name(session = session_name, theory = theory_name, name = export_name)
+            Entry_Name(session = session, theory = theory, name = export_name)
               .read(db, cache)
           }
 
         def focus(other_theory: String): Provider =
-          if (other_theory == theory_name) this
-          else Provider.database(db, cache, session_name, other_theory)
+          if (other_theory == theory) this
+          else Provider.database(db, cache, session, theory = other_theory)
 
         override def toString: String = db.toString
       }
diff -r ebbb7d6eb296 -r 3513fdfeb4d8 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Aug 03 12:25:37 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Wed Aug 03 12:58:17 2022 +0200
@@ -33,10 +33,10 @@
     val thys =
       sessions_structure.build_requirements(List(session_name)).flatMap(session =>
         using(store.open_database(session)) { db =>
+          val provider = Export.Provider.database(db, store.cache, session)
           for (theory <- Export.read_theory_names(db, session))
           yield {
             progress.echo("Reading theory " + theory)
-            val provider = Export.Provider.database(db, store.cache, session, theory)
             read_theory(provider, session, theory, cache = cache)
           }
         })
@@ -110,7 +110,7 @@
   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")
+      provider.focus(theory_name)(Export.THEORY_PREFIX + "parents")
         .map(entry => split_lines(entry.uncompressed.text))
     }
   }
@@ -124,25 +124,26 @@
     theory_name: String,
     cache: Term.Cache = Term.Cache.none
   ): Theory = {
+    val theory_provider = provider.focus(theory_name)
     val parents =
-      read_theory_parents(provider, theory_name) getOrElse
+      read_theory_parents(theory_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),
-        read_consts(provider),
-        read_axioms(provider),
-        read_thms(provider),
-        read_classes(provider),
-        read_locales(provider),
-        read_locale_dependencies(provider),
-        read_classrel(provider),
-        read_arities(provider),
-        read_constdefs(provider),
-        read_typedefs(provider),
-        read_datatypes(provider),
-        read_spec_rules(provider),
-        read_others(provider))
+        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)
   }
 
@@ -151,7 +152,7 @@
     val theory_name = Thy_Header.PURE
 
     using(store.open_database(session_name)) { db =>
-      val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
+      val provider = Export.Provider.database(db, store.cache, session_name)
       read(provider, session_name, theory_name)
     }
   }
diff -r ebbb7d6eb296 -r 3513fdfeb4d8 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Aug 03 12:25:37 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Aug 03 12:58:17 2022 +0200
@@ -126,13 +126,12 @@
         Par_List.map[Batch, List[(String, Node_Info)]](
           { case (session, thys) =>
               db_context.database(session) { db =>
-                val provider0 = Export.Provider.database(db, db_context.cache, session, "")
+                val provider = Export.Provider.database(db, db_context.cache, session)
                 val result =
                   for (thy_name <- thys) yield {
                     val theory =
                       if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
                       else {
-                        val provider = provider0.focus(thy_name)
                         if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
                           Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache)
                         }