clarified context for retrieval: more explicit types, with optional close() operation;

--- a/src/Pure/Thy/export.scala	Thu Aug 04 17:14:56 2022 +0200
+++ b/src/Pure/Thy/export.scala	Thu Aug 04 22:15:50 2022 +0200
@@ -334,6 +334,77 @@
   }
 
 
+  /* context for retrieval */
+
+  def context(db_context: Sessions.Database_Context): Context = new Context(db_context)
+
+  def open_context(store: Sessions.Store): Context =
+    new Context(store.open_database_context()) { override def close(): Unit = db_context.close() }
+
+  def open_context(options: Options): Context = open_context(Sessions.store(options))
+
+  class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable {
+    def close(): Unit = ()
+
+    def open_session(
+      session: String,
+      resources: Resources,
+      snapshot: Document.Snapshot = Document.Snapshot.init
+    ): Session_Context = {
+      val session_hierarchy = resources.sessions_structure.build_hierarchy(session)
+      db_context.database_server match {
+        case Some(db) =>
+          new Session_Context(resources, snapshot, db_context.cache, List(session -> db))
+        case None =>
+          val db_hierarchy = session_hierarchy.zip(db_context.store.open_databases(session_hierarchy))
+          new Session_Context(resources, snapshot, db_context.cache, db_hierarchy) {
+            override def close(): Unit = for ((_, db) <- this.db_hierarchy) db.close()
+          }
+      }
+    }
+
+    override def toString: String = db_context.toString
+  }
+
+  class Session_Context private[Export](
+    val resources: Resources,
+    val snapshot: Document.Snapshot,
+    val cache: Term.Cache,
+    val db_hierarchy: List[(String, SQL.Database)]
+  ) extends AutoCloseable {
+    session_context =>
+
+    def close(): Unit = ()
+
+    def get(theory: String, name: String): Option[Entry] =
+      snapshot.exports_map.get(name) orElse
+        db_hierarchy.view.map({ case (session, db) =>
+            Export.Entry_Name(session = session, theory = theory, name = name).read(db, cache)
+        }).collectFirst({ case Some(entry) => entry })
+
+    def apply(theory: String, name: String, permissive: Boolean = false): Entry =
+      get(theory, name) match {
+        case None if permissive => empty_entry(theory, name)
+        case None => error("Missing export entry " + quote(compound_name(theory, name)))
+        case Some(entry) => entry
+      }
+
+    def theory(theory: String): Theory_Context =
+      new Theory_Context(session_context, theory)
+
+    override def toString: String =
+      "Export.Session_Context(" + commas_quote(db_hierarchy.map(_._1)) + ")"
+  }
+
+  class Theory_Context private[Export](session_context: Session_Context, theory: String) {
+    def get(name: String): Option[Entry] = session_context.get(theory, name)
+    def apply(name: String, permissive: Boolean = false): Entry =
+      session_context.apply(theory, name, permissive = permissive)
+
+    override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
+  }
+
+
   /* export to file-system */
 
   def export_files(

--- a/src/Pure/Thy/sessions.scala	Thu Aug 04 17:14:56 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 04 22:15:50 2022 +0200
@@ -1200,7 +1200,7 @@
 
   class Database_Context private[Sessions](
     val store: Sessions.Store,
-    database_server: Option[SQL.Database]
+    val database_server: Option[SQL.Database]
   ) extends AutoCloseable {
     def cache: Term.Cache = store.cache
 
@@ -1369,9 +1369,21 @@
       }
     }
 
+    def bad_database(name: String): Nothing =
+      error("Missing build database for session " + quote(name))
+
     def open_database(name: String, output: Boolean = false): SQL.Database =
-      try_open_database(name, output = output) getOrElse
-        error("Missing build database for session " + quote(name))
+      try_open_database(name, output = output) getOrElse bad_database(name)
+
+    def open_databases(names: List[String]): List[SQL.Database] = {
+      val res = names.map(name => name -> try_open_database(name))
+      res.collectFirst({ case (name, None) => name }) match {
+        case None => res.map(_._2.get)
+        case Some(bad) =>
+          for ((_, Some(db)) <- res) db.close()
+          bad_database(bad)
+      }
+    }
 
     def clean_output(name: String): (Boolean, Boolean) = {
       val relevant_db =