# HG changeset patch
# User wenzelm
# Date 1689600702 -7200
# Node ID f6ec57648894f1861d2e4a3d875e3474aa471a2e
# Parent  2f16f23baefdb5d6ca916b6dbdbe58ebcfa68a99
reuse SSH.Server connection for database server;

diff -r 2f16f23baefd -r f6ec57648894 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Mon Jul 17 12:22:39 2023 +0200
+++ b/src/Pure/Thy/browser_info.scala	Mon Jul 17 15:31:42 2023 +0200
@@ -671,12 +671,13 @@
     store: Store,
     deps: Sessions.Deps,
     sessions: List[String],
-    progress: Progress = new Progress
+    progress: Progress = new Progress,
+    server: SSH.Server = SSH.no_server
   ): Unit = {
     val root_dir = browser_info.presentation_dir(store).absolute
     progress.echo("Presentation in " + root_dir)
 
-    using(Export.open_database_context(store)) { database_context =>
+    using(Export.open_database_context(store, server = server)) { database_context =>
       val context0 = context(deps.sessions_structure, root_dir = root_dir)
 
       val sessions1 =
diff -r 2f16f23baefd -r f6ec57648894 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Jul 17 12:22:39 2023 +0200
+++ b/src/Pure/Thy/export.scala	Mon Jul 17 15:31:42 2023 +0200
@@ -274,18 +274,25 @@
 
   /* context for database access */
 
-  def open_database_context(store: Store): Database_Context =
-    new Database_Context(store, store.maybe_open_database_server())
+  def open_database_context(store: Store, server: SSH.Server = SSH.no_server): Database_Context =
+    new Database_Context(store, store.maybe_open_database_server(server = server))
 
-  def open_session_context0(store: Store, session: String): Session_Context =
-    open_database_context(store).open_session0(session, close_database_context = true)
+  def open_session_context0(
+    store: Store,
+    session: String,
+    server: SSH.Server = SSH.no_server
+  ): Session_Context = {
+    open_database_context(store, server = server)
+      .open_session0(session, close_database_context = true)
+  }
 
   def open_session_context(
     store: Store,
     session_background: Sessions.Background,
-    document_snapshot: Option[Document.Snapshot] = None
+    document_snapshot: Option[Document.Snapshot] = None,
+    server: SSH.Server = SSH.no_server
   ): Session_Context = {
-    open_database_context(store).open_session(
+    open_database_context(store, server = server).open_session(
       session_background, document_snapshot = document_snapshot, close_database_context = true)
   }
 
diff -r 2f16f23baefd -r f6ec57648894 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jul 17 12:22:39 2023 +0200
+++ b/src/Pure/Tools/build.scala	Mon Jul 17 15:31:42 2023 +0200
@@ -228,7 +228,7 @@
           results.sessions_ok.filter(name => browser_info.enabled(results.info(name)))
         if (presentation_sessions.nonEmpty && !progress.stopped) {
           Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions,
-            progress = progress)
+            progress = progress, server = server)
         }
 
         if (!results.ok && (progress.verbose || !no_build)) {
diff -r 2f16f23baefd -r f6ec57648894 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Jul 17 12:22:39 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon Jul 17 15:31:42 2023 +0200
@@ -389,7 +389,7 @@
           val (document_output, document_errors) =
             try {
               if (build_errors.isInstanceOf[Exn.Res[_]] && result0.ok && info.documents.nonEmpty) {
-                using(Export.open_database_context(store)) { database_context =>
+                using(Export.open_database_context(store, server = server)) { database_context =>
                   val documents =
                     using(database_context.open_session(session_background)) {
                       session_context =>