clarified signature --- avoid repeated open_database on server;

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