--- a/src/Pure/Thy/sessions.scala Wed Nov 25 21:13:45 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Nov 26 12:21:45 2020 +0100
@@ -1190,6 +1190,12 @@
def close { database_server.foreach(_.close) }
+ def output_database[A](session: String)(f: SQL.Database => A): A =
+ database_server match {
+ case Some(db) => f(db)
+ case None => using(store.open_database(session, output = true))(f)
+ }
+
def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] =
{
val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
--- a/src/Pure/Tools/build_job.scala Wed Nov 25 21:13:45 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Nov 26 12:21:45 2020 +0100
@@ -232,16 +232,18 @@
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
{
- val documents =
- using(store.open_database_context(deps.sessions_structure))(db_context =>
- Presentation.build_documents(session_name, deps, db_context,
- output_sources = info.document_output,
- output_pdf = info.document_output,
- progress = progress,
- verbose = verbose))
- using(store.open_database(session_name, output = true))(db =>
- documents.foreach(_.write(db, session_name)))
- (documents.flatMap(_.log_lines), Nil)
+ using(store.open_database_context(deps.sessions_structure))(db_context =>
+ {
+ val documents =
+ Presentation.build_documents(session_name, deps, db_context,
+ output_sources = info.document_output,
+ output_pdf = info.document_output,
+ progress = progress,
+ verbose = verbose)
+ db_context.output_database(session_name)(db =>
+ documents.foreach(_.write(db, session_name)))
+ (documents.flatMap(_.log_lines), Nil)
+ })
}
(Nil, Nil)
}