# HG changeset patch
# User wenzelm
# Date 1659613461 -7200
# Node ID d0037f04bba0165963fe372b687265954b7a207f
# Parent  a0253e471aa4185845090b5c76cb18be85a9187f
clarified signature: Export.Provider knows its (accidental) theory_names;

diff -r a0253e471aa4 -r d0037f04bba0 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Aug 04 12:43:33 2022 +0200
+++ b/src/Pure/Thy/export.scala	Thu Aug 04 13:44:21 2022 +0200
@@ -258,19 +258,27 @@
   object Provider {
     def none: Provider =
       new Provider {
+        def theory_names: List[String] = Nil
         def apply(export_name: String): Option[Entry] = None
         def focus(other_theory: String): Provider = this
 
         override def toString: String = "none"
       }
 
-    def database(
-      db: SQL.Database,
-      cache: XML.Cache,
-      session: String,
-      theory: String = ""
-    ) : Provider = {
+    private def make_database(
+        db: SQL.Database,
+        cache: XML.Cache,
+        session: String,
+        theory: String,
+        _theory_names: Synchronized[Option[List[String]]]
+    ): Provider = {
       new Provider {
+        def theory_names: List[String] =
+          _theory_names.change_result { st =>
+            val res = st.getOrElse(read_theory_names(db, session))
+            (res, Some(res))
+          }
+
         def apply(export_name: String): Option[Entry] =
           if (theory.isEmpty) None
           else {
@@ -280,14 +288,30 @@
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory) this
-          else Provider.database(db, cache, session, theory = other_theory)
+          else make_database(db, cache, session, theory, _theory_names)
 
         override def toString: String = db.toString
       }
     }
 
-    def snapshot(snapshot: Document.Snapshot): Provider =
+    def database(
+      db: SQL.Database,
+      cache: XML.Cache,
+      session: String,
+      theory: String = ""
+    ): Provider = make_database(db, cache, session, theory, Synchronized(None))
+
+    def snapshot(
+      resources: Resources,
+      snapshot: Document.Snapshot
+    ): Provider =
       new Provider {
+        def theory_names: List[String] =
+          (for {
+            (name, _) <- snapshot.version.nodes.iterator
+            if name.is_theory && !resources.session_base.loaded_theory(name)
+          } yield name.theory).toList
+
         def apply(export_name: String): Option[Entry] =
           snapshot.exports_map.get(export_name)
 
@@ -297,7 +321,7 @@
             val node_name =
               snapshot.version.nodes.theory_name(other_theory) getOrElse
                 error("Bad theory " + quote(other_theory))
-            Provider.snapshot(snapshot.state.snapshot(node_name))
+            Provider.snapshot(resources, snapshot.state.snapshot(node_name))
           }
 
         override def toString: String = snapshot.toString
@@ -305,6 +329,8 @@
   }
 
   trait Provider {
+    def theory_names: List[String]
+
     def apply(export_name: String): Option[Entry]
 
     def uncompressed_yxml(export_name: String): XML.Body =
diff -r a0253e471aa4 -r d0037f04bba0 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu Aug 04 12:43:33 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu Aug 04 13:44:21 2022 +0200
@@ -34,7 +34,7 @@
       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))
+          for (theory <- provider.theory_names)
           yield {
             progress.echo("Reading theory " + theory)
             read_theory(provider, session, theory, cache = cache)