clarified signature: more operations;

--- a/src/Pure/Admin/build_log.scala	Sat Jul 15 14:06:53 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Jul 15 19:34:48 2023 +0200
@@ -829,24 +829,16 @@
       "Store(" + s + ")"
     }
 
-    def open_database(
-      user: String = options.string("build_log_database_user"),
-      password: String = options.string("build_log_database_password"),
-      database: String = options.string("build_log_database_name"),
-      host: String = options.string("build_log_database_host"),
-      port: Int = options.int("build_log_database_port"),
-      ssh: Option[SSH.Session] =
-        proper_string(options.string("build_log_ssh_host")).map(ssh_host =>
-          SSH.open_session(options,
-            host = ssh_host,
-            user = options.string("build_log_ssh_user"),
-            port = options.int("build_log_ssh_port"))),
-      ssh_close: Boolean = true
-    ): PostgreSQL.Database = {
-      PostgreSQL.open_database(
-        user = user, password = password, database = database, host = host, port = port,
-        ssh = ssh, ssh_close = ssh_close)
-    }
+    def open_database(server: SSH.Server = SSH.no_server): PostgreSQL.Database =
+      PostgreSQL.open_database_server(options, server = server,
+        user = options.string("build_log_database_user"),
+        password = options.string("build_log_database_password"),
+        database = options.string("build_log_database_name"),
+        host = options.string("build_log_database_host"),
+        port = options.int("build_log_database_port"),
+        ssh_host = options.string("build_log_ssh_host"),
+        ssh_port = options.int("build_log_ssh_port"),
+        ssh_user = options.string("build_log_ssh_user"))
 
     def snapshot_database(
       db: PostgreSQL.Database,

--- a/src/Pure/General/sql.scala	Sat Jul 15 14:06:53 2023 +0200
+++ b/src/Pure/General/sql.scala	Sat Jul 15 19:34:48 2023 +0200
@@ -575,52 +575,75 @@
 object PostgreSQL {
   type Source = SQL.Source
 
+  lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")
+
   val default_server: SSH.Server = SSH.local_server(port = 5432)
 
-  lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")
+  def open_database_server(
+    options: Options,
+    user: String = "",
+    password: String = "",
+    database: String = "",
+    host: String = "",
+    port: Int = 0,
+    ssh_host: String = "",
+    ssh_port: Int = 0,
+    ssh_user: String = "",
+    server: SSH.Server = SSH.no_server
+  ): PostgreSQL.Database = {
+    val (db_server, server_close) =
+      if (server.defined) (server, false)
+      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)
+      }
+
+    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 }
+  }
 
   def open_database(
     user: String,
     password: String,
     database: String = "",
-    host: String = "",
-    port: Int = 0,
-    ssh: Option[SSH.Session] = None,
-    ssh_close: Boolean = false,
+    server: SSH.Server = default_server,
+    server_close: Boolean = false,
     // see https://www.postgresql.org/docs/current/transaction-iso.html
     transaction_isolation: Int = Connection.TRANSACTION_SERIALIZABLE
   ): Database = {
     init_jdbc
 
-    if (user == "") error("Undefined database user")
-
-    val db_host = proper_string(host) getOrElse default_server.host
-    val db_port = if (port > 0) port else default_server.port
-    val db_name = proper_string(database) getOrElse user
+    if (user.isEmpty) error("Undefined database user")
+    if (server.host.isEmpty) error("Undefined database server host")
+    if (server.port <= 0) error("Undefined database server port")
 
-    val server =
-      ssh match {
-        case None =>
-          SSH.local_server(port = db_port, host = db_host)
-        case Some(ssh) =>
-          ssh.open_server(remote_port = db_port, remote_host = db_host, ssh_close = ssh_close)
-      }
-    try {
-      val url = "jdbc:postgresql://" + server.host + ":" + server.port + "/" + db_name
-      val name = user + "@" + server + "/" + db_name + if_proper(ssh, " via ssh " + ssh.get)
-      val connection = DriverManager.getConnection(url, user, password)
-      connection.setTransactionIsolation(transaction_isolation)
-      new Database(name, connection, server)
-    }
-    catch { case exn: Throwable => server.close(); throw exn }
+    val name = proper_string(database) getOrElse user
+    val url = "jdbc:postgresql://" + server.host + ":" + server.port + "/" + name
+    val ssh = server.ssh_system.ssh_session
+    val print = user + "@" + server + "/" + name + if_proper(ssh, " via ssh " + ssh.get)
+
+    val connection = DriverManager.getConnection(url, user, password)
+    connection.setTransactionIsolation(transaction_isolation)
+    new Database(connection, print, server, server_close)
   }
 
   class Database private[PostgreSQL](
-    name: String,
     val connection: Connection,
-    server: SSH.Server
+    print: String,
+    server: SSH.Server,
+    server_close: Boolean
   ) extends SQL.Database {
-    override def toString: String = name
+    override def toString: String = print
 
     override def now(): Date = {
       val now = SQL.Column.date("now")
@@ -671,6 +694,6 @@
       }
 
 
-    override def close(): Unit = { super.close(); server.close() }
+    override def close(): Unit = { super.close(); if (server_close) server.close() }
   }
 }

--- a/src/Pure/General/ssh.scala	Sat Jul 15 14:06:53 2023 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jul 15 19:34:48 2023 +0200
@@ -397,7 +397,7 @@
   class Server private[SSH](
     val host: String,
     val port: Int,
-    val system: System
+    val ssh_system: System
   ) extends AutoCloseable {
     def defined: Boolean = host.nonEmpty && port > 0
     override def close(): Unit = ()

--- a/src/Pure/Thy/store.scala	Sat Jul 15 14:06:53 2023 +0200
+++ b/src/Pure/Thy/store.scala	Sat Jul 15 19:34:48 2023 +0200
@@ -294,20 +294,16 @@
   def build_database_server: Boolean = options.bool("build_database_server")
   def build_database_test: Boolean = options.bool("build_database_test")
 
-  def open_database_server(): PostgreSQL.Database =
-    PostgreSQL.open_database(
+  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"),
       password = options.string("build_database_password"),
       database = options.string("build_database_name"),
       host = options.string("build_database_host"),
       port = options.int("build_database_port"),
-      ssh =
-        proper_string(options.string("build_database_ssh_host")).map(ssh_host =>
-          SSH.open_session(options,
-            host = ssh_host,
-            user = options.string("build_database_ssh_user"),
-            port = options.int("build_database_ssh_port"))),
-      ssh_close = true)
+      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 maybe_open_database_server(): Option[SQL.Database] =
     if (build_database_server) Some(open_database_server()) else None