src/Pure/General/ssh.scala

--- a/src/Pure/General/ssh.scala	Sat Apr 29 19:43:04 2017 +0200
+++ b/src/Pure/General/ssh.scala	Sat Apr 29 20:15:26 2017 +0200
@@ -134,16 +134,17 @@
 
   object Port_Forwarding
   {
-    def open(ssh: Session,
+    def open(ssh: Session, ssh_close: Boolean,
       local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding =
     {
       val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port)
-      new Port_Forwarding(ssh, local_host, port, remote_host, remote_port)
+      new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port)
     }
   }
 
   class Port_Forwarding private[SSH](
     ssh: SSH.Session,
+    ssh_close: Boolean,
     val local_host: String,
     val local_port: Int,
     val remote_host: String,
@@ -152,7 +153,11 @@
     override def toString: String =
       local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
 
-    def close() { ssh.session.delPortForwardingL(local_host, local_port) }
+    def close()
+    {
+      ssh.session.delPortForwardingL(local_host, local_port)
+      if (ssh_close) ssh.close()
+    }
   }
 
 
@@ -264,9 +269,11 @@
 
     /* port forwarding */
 
-    def port_forwarding(remote_port: Int, remote_host: String = "localhost",
-        local_port: Int = 0, local_host: String = "localhost"): Port_Forwarding =
-      Port_Forwarding.open(this, local_host, local_port, remote_host, remote_port)
+    def port_forwarding(
+        remote_port: Int, remote_host: String = "localhost",
+        local_port: Int = 0, local_host: String = "localhost",
+        ssh_close: Boolean = false): Port_Forwarding =
+      Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port)
 
 
     /* sftp channel */