# HG changeset patch
# User wenzelm
# Date 1663333068 -7200
# Node ID 5912209b4fb66479e5e780f1240c0e187eeaac97
# Parent  a3c694039fd67ca1dca292d778b30ffdfe0630a3
clarified modules;

diff -r a3c694039fd6 -r 5912209b4fb6 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Fri Sep 16 14:26:42 2022 +0200
+++ b/src/Pure/General/rsync.scala	Fri Sep 16 14:57:48 2022 +0200
@@ -14,14 +14,8 @@
     archive: Boolean = true,
     protect_args: Boolean = true  // requires rsync 3.0.0, or later
   ) {
-    require(ssh_control_path.isEmpty || ssh_control_path == Bash.string(ssh_control_path),
-      "Malformed socket path: " + quote(ssh_control_path))
-
     def command: String = {
-      val ssh_command =
-        "ssh" + (if (ssh_port > 0) " -p " + ssh_port else "") +
-        (if (ssh_control_path.nonEmpty) " -o ControlPath=" + ssh_control_path else "")
-
+      val ssh_command = SSH.client_command(port = ssh_port, control_path = ssh_control_path)
       "rsync --rsh=" + Bash.string(ssh_command) +
         (if (archive) " --archive" else "") +
         (if (protect_args) " --protect-args" else "")
diff -r a3c694039fd6 -r 5912209b4fb6 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Sep 16 14:26:42 2022 +0200
+++ b/src/Pure/General/ssh.scala	Fri Sep 16 14:57:48 2022 +0200
@@ -13,6 +13,17 @@
 
 
 object SSH {
+  /* client command */
+
+  def client_command(port: Int = 0, control_path: String = ""): String =
+    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 "")
+    }
+    else error ("Malformed SSH control socket: " + quote(control_path))
+
+
   /* OpenSSH configuration and command-line */
 
   // see https://linux.die.net/man/5/ssh_config
diff -r a3c694039fd6 -r 5912209b4fb6 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Sep 16 14:26:42 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala	Fri Sep 16 14:57:48 2022 +0200
@@ -896,10 +896,8 @@
   final class API private(ssh_target: String, ssh_port: Int) {
     /* connection */
 
-    require(ssh_target.nonEmpty && ssh_port >= 0, "bad ssh host or port")
-
     private def ssh_port_suffix: String =
-      if (ssh_port != default_system_port) ":" + ssh_port else ""
+      if (ssh_port > 0) ":" + ssh_port else ""
 
     override def toString: String = ssh_target + ssh_port_suffix
     def hg_url: String = "ssh://" + ssh_target + ssh_port_suffix