# HG changeset patch
# User wenzelm
# Date 1689515593 -7200
# Node ID aa4ea5398ab84017414ca2980980ab609128a474
# Parent  bb5e2a7198e330591a301b83e69226b96f79b671
clarified signature: more operations;

diff -r bb5e2a7198e3 -r aa4ea5398ab8 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 14:19:36 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 15:53:13 2023 +0200
@@ -633,37 +633,48 @@
 
   val default_server: SSH.Server = SSH.local_server(port = 5432)
 
+  def open_server(
+    options: Options,
+    host: String = "",
+    port: Int = 0,
+    ssh_host: String = "",
+    ssh_port: Int = 0,
+    ssh_user: String = ""
+  ): SSH.Server = {
+    val server_host = proper_string(host).getOrElse(default_server.host)
+    val server_port = if (port > 0) port else default_server.port
+
+    if (ssh_host.isEmpty) SSH.local_server(host = server_host, port = server_port)
+    else {
+      SSH.open_server(options, host = ssh_host, port = ssh_port, user = ssh_user,
+        remote_host = server_host, remote_port = server_port)
+    }
+  }
+
   def open_database_server(
     options: Options,
     user: String = "",
     password: String = "",
     database: String = "",
+    server: SSH.Server = SSH.no_server,
     host: String = "",
     port: Int = 0,
     ssh_host: String = "",
     ssh_port: Int = 0,
-    ssh_user: String = "",
-    server: SSH.Server = SSH.no_server
+    ssh_user: String = ""
   ): PostgreSQL.Database = {
-    val (db_server, server_close) =
-      if (server.defined) (server, false)
+    val db_server =
+      if (server.defined) server
       else {
-        val server_host = proper_string(host).getOrElse(default_server.host)
-        val server_port = if (port > 0) port else default_server.port
-        val db_server =
-          if (ssh_host.isEmpty) SSH.local_server(host = server_host, port = server_port)
-          else {
-            SSH.open_server(options, host = ssh_host, port = ssh_port, user = ssh_user,
-              remote_host = server_host, remote_port = server_port)
-          }
-        (db_server, true)
+        open_server(options, host = host, port = port, ssh_host = ssh_host,
+          ssh_port = ssh_port, ssh_user = ssh_user)
       }
-
+    val server_close = !server.defined
     try {
       open_database(user = user, password = password, database = database,
         server = db_server, server_close = server_close)
     }
-    catch { case exn: Throwable => if (server_close) db_server.close(); throw exn }
+    catch { case exn: Throwable if server_close => db_server.close(); throw exn }
   }
 
   def open_database(
diff -r bb5e2a7198e3 -r aa4ea5398ab8 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Sun Jul 16 14:19:36 2023 +0200
+++ b/src/Pure/Thy/store.scala	Sun Jul 16 15:53:13 2023 +0200
@@ -294,6 +294,14 @@
   def build_database_server: Boolean = options.bool("build_database_server")
   def build_database_test: Boolean = options.bool("build_database_test")
 
+  def open_server(): SSH.Server =
+    PostgreSQL.open_server(options,
+      host = options.string("build_database_host"),
+      port = options.int("build_database_port"),
+      ssh_host = options.string("build_database_ssh_host"),
+      ssh_port = options.int("build_database_ssh_port"),
+      ssh_user = options.string("build_database_ssh_user"))
+
   def open_database_server(server: SSH.Server = SSH.no_server): PostgreSQL.Database =
     PostgreSQL.open_database_server(options, server = server,
       user = options.string("build_database_user"),