src/Pure/General/mercurial.scala

 
     def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
 
     def sync(target: String,
       progress: Progress = new Progress,
+      port: Int = SSH.default_port,
       verbose: Boolean = false,
       thorough: Boolean = false,
       dry_run: Boolean = false,
       clean: Boolean = false,
       filter: List[String] = Nil,

             val source = File.standard_path(tmp_dir + Path.explode("archive"))
             archive(source, rev = rev)
             (Nil, source)
           }
         Isabelle_System.rsync(
-          progress = progress, verbose = verbose, thorough = thorough,
+          progress = progress, port = port, verbose = verbose, thorough = thorough,
           dry_run = dry_run, clean = clean, filter = filter,
           args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target))
       }
     }
 

         var filter: List[String] = Nil
         var root: Option[Path] = None
         var thorough = false
         var dry_run = false
         var rev = ""
+        var port = SSH.default_port
         var verbose = false
 
         val getopts = Getopts("""
 Usage: isabelle hg_sync [OPTIONS] TARGET
 

                  (default: implicit from current directory)
     -T           thorough treatment of file content and directory times
     -f           force changes: no dry-run
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
+    -p PORT      explicit SSH port (default: """ + SSH.default_port + """)
     -v           verbose
 
   Synchronize Mercurial repository with TARGET directory,
   which can be local or remote (using notation of rsync).
 """,

           "R:" -> (arg => root = Some(Path.explode(arg))),
           "T" -> (_ => thorough = true),
           "f" -> (_ => dry_run = false),
           "n" -> (_ => dry_run = true),
           "r:" -> (arg => rev = arg),
+          "p:" -> (arg => port = Value.Int.parse(arg)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
         val target =
           more_args match {

         val hg =
           root match {
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        hg.sync(target, progress = progress, verbose = verbose, thorough = thorough,
+        hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
           dry_run = dry_run, clean = clean, filter = filter, rev = rev)
       }
     )
 }