src/Pure/General/ssh.scala

       (if (user.nonEmpty) List(entry("User", user)) else Nil) :::
       (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) :::
       (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil)
     }
 
-    def make_command(command: String, config: List[String]): String =
-      Bash.string(command) + " " + config.map(entry => "-o " + Bash.string(entry)).mkString(" ")
+    def option(entry: String): String = "-o " + Bash.string(entry)
+    def option(x: String, y: String): String = option(entry(x, y))
+    def option(x: String, y: Int): String = option(entry(x, y))
+    def option(x: String, y: Boolean): String = option(entry(x, y))
+
+    def command(command: String, config: List[String]): String =
+      Bash.string(command) + config.map(entry => " " + option(entry)).mkString
   }
 
   def sftp_string(str: String): String = {
     val special = Set(' ', '*', '?', '{', '}')
     if (str.exists(special)) {

     multiplex: Boolean = !Platform.is_windows
   ): Session = {
     val (control_master, control_path) =
       if (multiplex) (true, Isabelle_System.tmp_file("ssh_socket", initialized = false).getPath)
       else (false, "")
-
     new Session(options, host, port, user, control_master, control_path)
   }
 
   class Session private[SSH](
     val options: Options,

     override def toString: String = user_prefix + host + port_suffix
     override def hg_url: String = "ssh://" + toString + "/"
     override def rsync_prefix: String = user_prefix + host + ":"
 
 
-    /* ssh commands */
+    /* local ssh commands */
 
     def run_command(command: String,
       master: Boolean = false,
       opts: String = "",
       args: String = "",

     ): Process_Result = {
       val config =
         Config.make(options, port = port, user = user,
           control_master = master, control_path = control_path)
       val cmd =
-        Config.make_command(command, config) +
+        Config.command(command, config) +
         (if (opts.nonEmpty) " " + opts else "") +
         (if (args.nonEmpty) " -- " + args else "")
       Isabelle_System.bash(cmd, progress_stdout = progress_stdout,
         progress_stderr = progress_stderr, strict = strict)
     }

       remote_host: String = "localhost",
       local_port: Int = 0,
       local_host: String = "localhost",
       ssh_close: Boolean = false
     ): Port_Forwarding = {
-      if (control_path.isEmpty) error("SSH port forwarding requires multiplexing")
-
       val port = if (local_port > 0) local_port else Isabelle_System.local_port()
 
-      val string = List(local_host, port, remote_host, remote_port).mkString(":")
-      run_ssh(opts = "-L " + Bash.string(string) + " -O forward").check
+      val forward = List(local_host, port, remote_host, remote_port).mkString(":")
+      val forward_option = "-L " + Bash.string(forward)
+
+      val cancel: () => Unit =
+        if (control_path.nonEmpty) {
+          run_ssh(opts = forward_option + " -O forward").check
+          () => run_ssh(opts = forward_option + " -O cancel")  // permissive
+        }
+        else error("SSH port forwarding requires multiplexing")
+
+      val shutdown_hook =
+        Isabelle_System.create_shutdown_hook { cancel() }
 
       new Port_Forwarding(host, port, remote_host, remote_port) {
-        override def toString: String = string
+        override def toString: String = forward
         override def close(): Unit = {
-          run_ssh(opts = "-L " + Bash.string(string) + " -O cancel").check
+          cancel()
+          Isabelle_System.remove_shutdown_hook(shutdown_hook)
           if (ssh_close) ssh.close()
         }
       }
     }
   }