clarified default: do not override port from ssh_config, which could be different from 22;

--- a/src/Doc/System/Misc.thy	Tue Sep 13 09:45:02 2022 +0200
+++ b/src/Doc/System/Misc.thy	Tue Sep 13 09:59:08 2022 +0200
@@ -319,7 +319,7 @@
     -T           thorough treatment of file content and directory times
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
-    -p PORT      explicit SSH port (default: 22)
+    -p PORT      explicit SSH port
     -v           verbose
 
   Synchronize Mercurial repository with TARGET directory,
@@ -354,7 +354,7 @@
   equal, and to ignore time stamps on directories.
 
   \<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
-  \<^verbatim>\<open>rsync\<close>.
+  \<^verbatim>\<open>rsync\<close>; the default is taken from the user's \<^path>\<open>ssh_config\<close> file.
 
   \<^medskip> Option \<^verbatim>\<open>-S\<close> uses \<^verbatim>\<open>rsync --protect-args\<close> to work robustly with spaces or
   special characters of the shell. This requires at least \<^verbatim>\<open>rsync 3.0.0\<close>,

--- a/src/Doc/System/Sessions.thy	Tue Sep 13 09:45:02 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Sep 13 09:59:08 2022 +0200
@@ -937,7 +937,7 @@
     -a REV       explicit AFP revision (default: state of working directory)
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
-    -p PORT      explicit SSH port (default: 22)
+    -p PORT      explicit SSH port
     -v           verbose
 
   Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\<close>}

--- a/src/Pure/General/mercurial.scala	Tue Sep 13 09:45:02 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Sep 13 09:59:08 2022 +0200
@@ -566,7 +566,7 @@
         var thorough = false
         var dry_run = false
         var rev = ""
-        var port = SSH.default_port
+        var port = 0
         var verbose = false
 
         val getopts = Getopts("""
@@ -582,7 +582,7 @@
     -T           thorough treatment of file content and directory times
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
-    -p PORT      explicit SSH port (default: """ + SSH.default_port + """)
+    -p PORT      explicit SSH port
     -v           verbose
 
   Synchronize Mercurial repository with TARGET directory,

--- a/src/Pure/General/rsync.scala	Tue Sep 13 09:45:02 2022 +0200
+++ b/src/Pure/General/rsync.scala	Tue Sep 13 09:59:08 2022 +0200
@@ -9,12 +9,12 @@
 
 object Rsync {
   sealed case class Context(progress: Progress,
-    port: Int = SSH.default_port,
+    port: Int = 0,
     archive: Boolean = true,
     protect_args: Boolean = true  // requires rsync 3.0.0, or later
   ) {
     def command: String =
-      "rsync --rsh=" + Bash.string("ssh -p " + port) +
+      "rsync --rsh=" + Bash.string("ssh" + (if (port > 0) "-p " + port else "")) +
         (if (archive) " --archive" else "") +
         (if (protect_args) " --protect-args" else "")
   }

--- a/src/Pure/General/ssh.scala	Tue Sep 13 09:45:02 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 09:59:08 2022 +0200
@@ -28,17 +28,9 @@
     }
   }
 
-  val default_port = 22
-  def make_port(port: Int): Int = if (port > 0) port else default_port
-
-  def port_suffix(port: Int): String =
-    if (port == default_port) "" else ":" + port
+  def port_suffix(port: Int): String = if (port > 0) ":" + port else ""
 
-  def user_prefix(user: String): String =
-    proper_string(user) match {
-      case None => ""
-      case Some(name) => name + "@"
-    }
+  def user_prefix(user: String): String = if (user.nonEmpty) user + "@" else ""
 
 
   /* OpenSSH configuration and command-line */
@@ -50,7 +42,7 @@
     def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no")
 
     def make(options: Options,
-      port: Int = default_port,
+      port: Int = 0,
       user: String = "",
       control_master: Boolean = false,
       control_path: String = ""
@@ -60,7 +52,7 @@
         entry("ServerAliveInterval", options.seconds("ssh_alive_interval").ms.toInt),
         entry("ServerAliveCountMax", options.int("ssh_alive_count_max")),
         entry("Compression", options.bool("ssh_compression"))) :::
-      (if (port > 0 && port != default_port) List(entry("Port", port)) else Nil) :::
+      (if (port > 0) List(entry("Port", port)) else Nil) :::
       (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)
@@ -101,7 +93,7 @@
       }
       else (false, "")
 
-    new Session(options, host, make_port(port), user, control_master, control_path)
+    new Session(options, host, port, user, control_master, control_path)
   }
 
   class Session private[SSH](

--- a/src/Pure/Tools/sync.scala	Tue Sep 13 09:45:02 2022 +0200
+++ b/src/Pure/Tools/sync.scala	Tue Sep 13 09:59:08 2022 +0200
@@ -89,7 +89,7 @@
         var afp_rev = ""
         var dry_run = false
         var rev = ""
-        var port = SSH.default_port
+        var port = 0
         var verbose = false
 
         val getopts = Getopts("""
@@ -107,7 +107,7 @@
     -a REV       explicit AFP revision (default: state of working directory)
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
-    -p PORT      explicit SSH port (default: """ + SSH.default_port + """)
+    -p PORT      explicit SSH port
     -v           verbose
 
   Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".