# HG changeset patch
# User wenzelm
# Date 1659448428 -7200
# Node ID 6b319113b3a4a518b68ef81ba36c762af08e6d27
# Parent  5934209c49072d3dfa3f6daef368753bd017222c
clarified signature: avoid repeated db_context.input_database;

diff -r 5934209c4907 -r 6b319113b3a4 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Aug 02 15:49:57 2022 +0200
+++ b/src/Pure/Thy/export.scala	Tue Aug 02 15:53:48 2022 +0200
@@ -264,19 +264,6 @@
         override def toString: String = "none"
       }
 
-    def database_context(
-        context: Sessions.Database_Context,
-        session_hierarchy: List[String],
-        theory_name: String): Provider =
-      new Provider {
-        def apply(export_name: String): Option[Entry] =
-          context.read_export(session_hierarchy, theory_name, export_name)
-
-        def focus(other_theory: String): Provider = this
-
-        override def toString: String = context.toString
-      }
-
     def database(
       db: SQL.Database,
       cache: XML.Cache,
diff -r 5934209c4907 -r 6b319113b3a4 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Tue Aug 02 15:49:57 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Tue Aug 02 15:53:48 2022 +0200
@@ -125,18 +125,23 @@
       val theory_node_info =
         Par_List.map[Batch, List[(String, Node_Info)]](
           { case (session, thys) =>
-              for (thy_name <- thys) yield {
-                val theory =
-                  if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
-                  else {
-                    val provider = Export.Provider.database_context(db_context, List(session), thy_name)
-                    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
+              db_context.input_database(session) { (db, _) =>
+                val provider0 = 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)
+                        }
+                        else Export_Theory.no_theory
+                      }
+                    thy_name -> Node_Info.make(theory)
                   }
-                thy_name -> Node_Info.make(theory)
-              }
+                Some(result)
+              } getOrElse Nil
           }, batches).flatten.toMap
       new Nodes(theory_node_info)
     }