src/Pure/General/ssh.scala

--- a/src/Pure/General/ssh.scala	Wed Mar 18 22:22:16 2020 +0100
+++ b/src/Pure/General/ssh.scala	Thu Mar 19 11:27:54 2020 +0100
@@ -83,10 +83,12 @@
     new Context(options, jsch)
   }
 
-  def open_session(options: Options, host: String, user: String = "", port: Int = 0,
+  def open_session(options: Options,
+      host: String, user: String = "", port: Int = 0, actual_host: String = "",
       proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
       permissive: Boolean = false): Session =
-    init_context(options).open_session(host = host, user = user, port = port,
+    init_context(options).open_session(
+      host = host, user = user, port = port, actual_host = actual_host,
       proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
       permissive = permissive)
 
@@ -120,16 +122,18 @@
         proper_string(nominal_user) getOrElse user)
     }
 
-    def open_session(host: String, user: String = "", port: Int = 0,
+    def open_session(
+      host: String, user: String = "", port: Int = 0, actual_host: String = "",
       proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
       permissive: Boolean = false): Session =
     {
-      if (proxy_host == "") connect_session(host = host, user = user, port = port)
+      val connect_host = proper_string(actual_host) getOrElse host
+      if (proxy_host == "") connect_session(host = connect_host, user = user, port = port)
       else {
         val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
 
         val fw =
-          try { proxy.port_forwarding(remote_host = host, remote_port = make_port(port)) }
+          try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
           catch { case exn: Throwable => proxy.close; throw exn }
 
         try {