src/Pure/General/ssh.scala

--- a/src/Pure/General/ssh.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/General/ssh.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -19,7 +19,7 @@
     if (control_path.isEmpty || control_path == Bash.string(control_path)) {
       "ssh" +
         (if (port > 0) " -p " + port else "") +
-        (if (control_path.nonEmpty) " -o ControlPath=" + control_path else "")
+        if_proper(control_path, " -o ControlPath=" + control_path)
     }
     else error ("Malformed SSH control socket: " + quote(control_path))
 
@@ -130,8 +130,8 @@
           control_master = master, control_path = control_path)
       val cmd =
         Config.command(command, config) +
-        (if (opts.nonEmpty) " " + opts else "") +
-        (if (args.nonEmpty) " -- " + args else "")
+        if_proper(opts, " " + opts) +
+        if_proper(args, " -- " + args)
       Isabelle_System.bash(cmd, cwd = cwd,
         redirect = redirect,
         progress_stdout = progress_stdout,
@@ -155,7 +155,7 @@
     }
 
     def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
-      val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
+      val args1 = Bash.string(host) + if_proper(args, " " + args)
       run_command("ssh", master = master, opts = opts, args = args1)
     }