# HG changeset patch
# User wenzelm
# Date 1689334265 -7200
# Node ID 5790e48f7573efb11006c06eb5fc00f61fd43efa
# Parent  f8a553a2142345ce2f34e20475333d7b43de998f
clarified signature: more uniform SSH.Port_Forwarding;

diff -r f8a553a21423 -r 5790e48f7573 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Jul 14 11:11:06 2023 +0200
+++ b/src/Pure/General/sql.scala	Fri Jul 14 13:31:05 2023 +0200
@@ -598,34 +598,30 @@
     val db_port = if (port > 0 && port != default_port) ":" + port else ""
     val db_name = "/" + (proper_string(database) getOrElse user)
 
-    val (url, name, port_forwarding) =
+    val fw =
       ssh match {
         case None =>
-          val spec = db_host + db_port + db_name
-          val url = "jdbc:postgresql://" + spec
-          val name = user + "@" + spec
-          (url, name, None)
+          SSH.no_port_forwarding(port = if (port > 0) port else default_port, host = db_host)
         case Some(ssh) =>
-          val fw =
-            ssh.port_forwarding(remote_host = db_host,
-              remote_port = if (port > 0) port else default_port,
-              ssh_close = ssh_close)
-          val url = "jdbc:postgresql://localhost:" + fw.port + db_name
-          val name = user + "@" + fw + db_name + " via ssh " + ssh
-          (url, name, Some(fw))
+          ssh.port_forwarding(
+            remote_port = if (port > 0) port else default_port,
+            remote_host = db_host,
+            ssh_close = ssh_close)
       }
     try {
+      val url = "jdbc:postgresql://" + fw.host + ":" + fw.port + db_name
+      val name = user + "@" + fw + db_name + if_proper(ssh, " via ssh " + ssh.get)
       val connection = DriverManager.getConnection(url, user, password)
       connection.setTransactionIsolation(transaction_isolation)
-      new Database(name, connection, port_forwarding)
+      new Database(name, connection, fw)
     }
-    catch { case exn: Throwable => port_forwarding.foreach(_.close()); throw exn }
+    catch { case exn: Throwable => fw.close(); throw exn }
   }
 
   class Database private[PostgreSQL](
     name: String,
     val connection: Connection,
-    port_forwarding: Option[SSH.Port_Forwarding]
+    val port_forwarding: SSH.Port_Forwarding
   ) extends SQL.Database {
     override def toString: String = name
 
@@ -678,6 +674,6 @@
       }
 
 
-    override def close(): Unit = { super.close(); port_forwarding.foreach(_.close()) }
+    override def close(): Unit = { super.close(); port_forwarding.close() }
   }
 }
diff -r f8a553a21423 -r 5790e48f7573 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Jul 14 11:11:06 2023 +0200
+++ b/src/Pure/General/ssh.scala	Fri Jul 14 13:31:05 2023 +0200
@@ -323,9 +323,9 @@
       local_host: String = "localhost",
       ssh_close: Boolean = false
     ): Port_Forwarding = {
-      val port = if (local_port > 0) local_port else Isabelle_System.local_port()
-
-      val forward = List(local_host, port, remote_host, remote_port).mkString(":")
+      val forward_host = local_host
+      val forward_port = if (local_port > 0) local_port else Isabelle_System.local_port()
+      val forward = List(forward_host, forward_port, remote_host, remote_port).mkString(":")
       val forward_option = "-L " + Bash.string(forward)
 
       val cancel: () => Unit =
@@ -357,7 +357,7 @@
       val shutdown_hook =
         Isabelle_System.create_shutdown_hook { cancel() }
 
-      new Port_Forwarding(host, port, remote_host, remote_port) {
+      new Port_Forwarding(forward_host, forward_port) {
         override def toString: String = forward
         override def close(): Unit = {
           cancel()
@@ -368,11 +368,17 @@
     }
   }
 
+  def no_port_forwarding(port: Int = 0, host: String = "localhost"): Port_Forwarding = {
+    val forward = if_proper(host, host + ":") + port
+    new Port_Forwarding(host, port) {
+      override def toString: String = forward
+      override def close(): Unit = ()
+    }
+  }
+
   abstract class Port_Forwarding private[SSH](
     val host: String,
-    val port: Int,
-    val remote_host: String,
-    val remote_port: Int
+    val port: Int
   ) extends AutoCloseable