# HG changeset patch
# User wenzelm
# Date 1663160341 -7200
# Node ID 769ebb139a3209ae98315278a2a584613fc12576
# Parent  75f0fc965539d1b8bca8aba0b9983040b39e9e61
support port forwarding without multiplexing (for the sake of Windows);

diff -r 75f0fc965539 -r 769ebb139a32 etc/options
--- a/etc/options	Wed Sep 14 14:54:21 2022 +0200
+++ b/etc/options	Wed Sep 14 14:59:01 2022 +0200
@@ -289,6 +289,9 @@
 
 section "Secure Shell"
 
+option ssh_multiplexing : bool = true
+  -- "enable multiplexing of SSH sessions (ignored on Windows)"
+
 option ssh_compression : bool = true
   -- "enable SSH compression"
 
diff -r 75f0fc965539 -r 769ebb139a32 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Sep 14 14:54:21 2022 +0200
+++ b/src/Pure/General/ssh.scala	Wed Sep 14 14:59:01 2022 +0200
@@ -83,9 +83,9 @@
     options: Options,
     host: String,
     port: Int = 0,
-    user: String = "",
-    multiplex: Boolean = !Platform.is_windows
+    user: String = ""
   ): Session = {
+    val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows
     val (control_master, control_path) =
       if (multiplex) (true, Isabelle_System.tmp_file("ssh_socket", initialized = false).getPath)
       else (false, "")
@@ -265,7 +265,26 @@
           run_ssh(opts = forward_option + " -O forward").check
           () => run_ssh(opts = forward_option + " -O cancel")  // permissive
         }
-        else error("SSH port forwarding requires multiplexing")
+        else {
+          val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false))
+          val thread = Isabelle_Thread.fork("port_forwarding") {
+            val opts =
+              forward_option +
+                " " + Config.option("SessionType", "none") +
+                " " + Config.option("PermitLocalCommand", true) +
+                " " + Config.option("LocalCommand", "pwd")
+            try {
+              run_command("ssh", opts = opts, args = Bash.string(host),
+                progress_stdout = _ => result.change(_ => Exn.Res(true))).check
+            }
+            catch { case exn: Throwable => result.change(_ => Exn.Exn(exn)) }
+          }
+          result.guarded_access {
+            case res@Exn.Res(ok) => if (ok) Some((), res) else None
+            case Exn.Exn(exn) => throw exn
+          }
+          () => thread.interrupt()
+        }
 
       val shutdown_hook =
         Isabelle_System.create_shutdown_hook { cancel() }