# HG changeset patch
# User wenzelm
# Date 1661436333 -7200
# Node ID b4a04fa0167787640cb623a7756787ecc2515d5b
# Parent  0548beacff68ecda54f7891aec162514928c22ed
tuned signature: more general operations;

diff -r 0548beacff68 -r b4a04fa01677 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Aug 25 15:58:17 2022 +0200
+++ b/src/Pure/Thy/export.scala	Thu Aug 25 16:05:33 2022 +0200
@@ -277,11 +277,11 @@
 
     def close(): Unit = database_server.foreach(_.close())
 
-    def open_output_database(session: String): Session_Database =
+    def open_database(session: String, output: Boolean = false): Session_Database =
       database_server match {
         case Some(db) => new Session_Database(session, db)
         case None =>
-          new Session_Database(session, store.open_database(session, output = true)) {
+          new Session_Database(session, store.open_database(session, output = output)) {
             override def close(): Unit = db.close()
           }
       }
diff -r 0548beacff68 -r b4a04fa01677 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Aug 25 15:58:17 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Thu Aug 25 16:05:33 2022 +0200
@@ -456,7 +456,7 @@
                       output_sources = info.document_output,
                       output_pdf = info.document_output)
                 }
-              using(database_context.open_output_database(session_name))(session_database =>
+              using(database_context.open_database(session_name, output = true))(session_database =>
                 documents.foreach(_.write(session_database.db, session_name)))
               (documents.flatMap(_.log_lines), Nil)
             }