--- 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()
}
}
--- 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)
}