# HG changeset patch # User wenzelm # Date 1606389705 -3600 # Node ID 2615b8c053373488bcea22903966441910f7d3e1 # Parent fabd29c73098bbd91870ca15883fcdf7c9f12858 clarified signature --- avoid repeated open_database on server; diff -r fabd29c73098 -r 2615b8c05337 src/Pure/Thy/sessions.scala --- 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 diff -r fabd29c73098 -r 2615b8c05337 src/Pure/Tools/build_job.scala --- 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) }