src/Pure/General/ssh.scala
changeset 78341 5f14f1290a88
parent 78340 5790e48f7573
child 78345 545da61f5989
--- 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 */