clarified signature;

--- a/src/Pure/General/sql.scala	Fri Jul 14 13:31:05 2023 +0200
+++ b/src/Pure/General/sql.scala	Fri Jul 14 14:21:22 2023 +0200
@@ -601,7 +601,7 @@
     val fw =
       ssh match {
         case None =>
-          SSH.no_port_forwarding(port = if (port > 0) port else default_port, host = db_host)
+          SSH.local_port_forwarding(port = if (port > 0) port else default_port, host = db_host)
         case Some(ssh) =>
           ssh.port_forwarding(
             remote_port = if (port > 0) port else default_port,

--- a/src/Pure/General/ssh.scala	Fri Jul 14 13:31:05 2023 +0200
+++ b/src/Pure/General/ssh.scala	Fri Jul 14 14:21:22 2023 +0200
@@ -368,18 +368,27 @@
     }
   }
 
-  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 = ()
-    }
+  class Port_Forwarding private[SSH](
+    val host: String,
+    val port: Int
+  ) extends AutoCloseable {
+    def defined: Boolean = host.nonEmpty && port > 0
+    override def close(): Unit = ()
   }
 
-  abstract class Port_Forwarding private[SSH](
-    val host: String,
-    val port: Int
-  ) extends AutoCloseable
+  class Local_Port_Forwarding private[SSH](host: String, port: Int)
+    extends Port_Forwarding(host, port) {
+    override def toString: String = if_proper(host, host + ":") + port
+  }
+
+  class No_Port_Forwarding extends Port_Forwarding("", 0) {
+    override def toString: String = "0"
+  }
+
+  def local_port_forwarding(port: Int = 0, host: String = "localhost"): Port_Forwarding =
+    new Local_Port_Forwarding(host, port)
+
+  val no_port_forwarding: Port_Forwarding = new No_Port_Forwarding
 
 
   /* system operations */