# HG changeset patch
# User wenzelm
# Date 1659703487 -7200
# Node ID 07e097f60b850603634fb6d88ebd4508068a9148
# Parent  8cf14d4ebec47b8ebc60bbd3529ab8b23370e234
clarified signature: more robust close operation;

diff -r 8cf14d4ebec4 -r 07e097f60b85 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 14:05:42 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 14:44:47 2022 +0200
@@ -343,6 +343,10 @@
 
   def open_context(options: Options): Context = open_context(Sessions.store(options))
 
+  class Session_Database private[Export](val session: String, val db: SQL.Database) {
+    def close(): Unit = ()
+  }
+
   class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable {
     def close(): Unit = ()
 
@@ -354,11 +358,25 @@
       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))
+          val session_database = new Session_Database(session, db)
+          new Session_Context(resources, snapshot, db_context.cache, List(session_database))
         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()
+          val store = db_context.store
+          val session_databases = {
+            val res = session_hierarchy.map(name => name -> store.try_open_database(name))
+            res.collectFirst({ case (name, None) => name }) match {
+              case None =>
+                for ((name, Some(db)) <- res)
+                yield {
+                  new Session_Database(name, db) { override def close(): Unit = this.db.close() }
+                }
+              case Some(bad) =>
+                for ((_, Some(db)) <- res) db.close()
+                store.bad_database(bad)
+            }
+          }
+          new Session_Context(resources, snapshot, db_context.cache, session_databases) {
+            override def close(): Unit = db_hierarchy.foreach(_.close())
           }
       }
     }
@@ -370,7 +388,7 @@
     val resources: Resources,
     val snapshot: Document.Snapshot,
     val cache: Term.Cache,
-    val db_hierarchy: List[(String, SQL.Database)]
+    val db_hierarchy: List[Session_Database]
   ) extends AutoCloseable {
     session_context =>
 
@@ -378,9 +396,10 @@
 
     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 })
+        db_hierarchy.view.map(session_db =>
+          Export.Entry_Name(session = session_db.session, theory = theory, name = name)
+            .read(session_db.db, cache))
+          .collectFirst({ case Some(entry) => entry })
 
     def apply(theory: String, name: String, permissive: Boolean = false): Entry =
       get(theory, name) match {
@@ -393,7 +412,7 @@
       new Theory_Context(session_context, theory)
 
     override def toString: String =
-      "Export.Session_Context(" + commas_quote(db_hierarchy.map(_._1)) + ")"
+      "Export.Session_Context(" + commas_quote(db_hierarchy.map(_.session)) + ")"
   }
 
   class Theory_Context private[Export](session_context: Session_Context, theory: String) {
diff -r 8cf14d4ebec4 -r 07e097f60b85 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Aug 05 14:05:42 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 05 14:44:47 2022 +0200
@@ -1377,16 +1377,6 @@
     def open_database(name: String, output: Boolean = false): SQL.Database =
       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 =
         database_server && {