# HG changeset patch
# User wenzelm
# Date 1659868209 -7200
# Node ID f9fcf06aa2ebdea943753da276c069c17c23fb5e
# Parent  ff6c1a82270fe3683dd5ba328ec1888c9b2a6551
clarified signature;

diff -r ff6c1a82270f -r f9fcf06aa2eb src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 07 12:22:43 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 07 12:30:09 2022 +0200
@@ -243,7 +243,8 @@
 
   /* context for database access */
 
-  class Session_Database private[Export](val session: String, val db: SQL.Database) {
+  class Session_Database private[Export](val session: String, val db: SQL.Database)
+  extends AutoCloseable {
     def close(): Unit = ()
 
     lazy val theory_names: List[String] = read_theory_names(db, session)
@@ -286,10 +287,13 @@
 
     def close(): Unit = database_server.foreach(_.close())
 
-    def database_output[A](session: String)(f: SQL.Database => A): A =
+    def open_output_database(session: String): Session_Database =
       database_server match {
-        case Some(db) => f(db)
-        case None => using(store.open_database(session, output = true))(f)
+        case Some(db) => new Session_Database(session, db)
+        case None =>
+          new Session_Database(session, store.open_database(session, output = true)) {
+            override def close(): Unit = db.close()
+          }
       }
 
     def open_session0(session: String, close_database_context: Boolean = false): Session_Context =
diff -r ff6c1a82270f -r f9fcf06aa2eb src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Aug 07 12:22:43 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sun Aug 07 12:30:09 2022 +0200
@@ -450,8 +450,8 @@
                       output_sources = info.document_output,
                       output_pdf = info.document_output)
                 }
-              database_context.database_output(session_name)(db =>
-                documents.foreach(_.write(db, session_name)))
+              using(database_context.open_output_database(session_name))(session_database =>
+                documents.foreach(_.write(session_database.db, session_name)))
               (documents.flatMap(_.log_lines), Nil)
             }
           }