support for "isabelle hg_sync";

--- a/src/Pure/General/mercurial.scala	Sun May 29 13:06:30 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 29 13:13:45 2022 +0200
@@ -136,6 +136,10 @@
     find(ssh.expand_path(start))
   }
 
+  def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository =
+    find_repository(start, ssh = ssh) getOrElse
+      error("No repository found in " + start.absolute)
+
   private def make_repository(
     root: Path,
     cmd: String,
@@ -247,6 +251,23 @@
 
     def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
 
+    def sync(target: String,
+      progress: Progress = new Progress,
+      verbose: Boolean = false,
+      dry_run: Boolean = false,
+      clean: Boolean = false
+    ): Unit = {
+      Isabelle_System.with_tmp_file("exclude") { exclude_path =>
+        val exclude = status(options = "--unknown --ignored --no-status")
+        File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
+        Isabelle_System.rsync(
+          progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
+          args = List("--prune-empty-dirs", "--exclude-from=" + exclude_path.implode,
+            "--", ssh.rsync_url + root.expand.implode + "/.", target)
+        ).check
+      }
+    }
+
     def graph(): Graph = {
       val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
       val log_result =
@@ -403,7 +424,7 @@
     local_hg.push(remote = remote_url)
   }
 
-  val isabelle_tool =
+  val isabelle_tool1 =
     Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
       Scala_Project.here,
       { args =>
@@ -439,4 +460,54 @@
         hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
           remote_exists = remote_exists, progress = progress)
       })
+
+
+
+  /** hg_sync **/
+
+  val isabelle_tool2 =
+    Isabelle_Tool("hg_sync", "synchronize Mercurial repository working directory",
+      Scala_Project.here, { args =>
+        var clean = false
+        var root: Option[Path] = None
+        var dry_run = false
+        var verbose = false
+
+        val getopts = Getopts("""
+Usage: isabelle hg_sync [OPTIONS] TARGET
+
+  Options are:
+    -C           clean all unknown/ignored files on target
+                 (potentially DANGEROUS: use with option -f to confirm)
+    -R ROOT      explicit repository root directory
+                 (default: implicit from current directory)
+    -f           force changes: no dry-run
+    -n           no changes: dry-run
+    -v           verbose
+
+  Synchronize Mercurial repository working directory with other TARGET,
+  which can be local or remote (using notation of rsync).
+""",
+          "C" -> { _ => clean = true; dry_run = true },
+          "R:" -> (arg => root = Some(Path.explode(arg))),
+          "f" -> (_ => dry_run = false),
+          "n" -> (_ => dry_run = true),
+          "v" -> (_ => verbose = true))
+
+        val more_args = getopts(args)
+        val target =
+          more_args match {
+            case List(target) => target
+            case _ => getopts.usage()
+          }
+
+        val progress = new Console_Progress
+        val hg =
+          root match {
+            case Some(dir) => repository(dir)
+            case None => the_repository(Path.current)
+          }
+        hg.sync(target, verbose = verbose, dry_run = dry_run, clean = clean, progress = progress)
+      }
+    )
 }

--- a/src/Pure/General/ssh.scala	Sun May 29 13:06:30 2022 +0200
+++ b/src/Pure/General/ssh.scala	Sun May 29 13:13:45 2022 +0200
@@ -40,8 +40,8 @@
   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, suffix: String = ":"): String =
+    if (port == default_port) "" else suffix + port
 
   def user_prefix(user: String): String =
     proper_string(user) match {
@@ -328,6 +328,9 @@
     override def hg_url: String =
       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
 
+    override def rsync_url: String = ""
+      user_prefix(nominal_user) + nominal_host + ":" + port_suffix(port, suffix = "") + "/"
+
     override def toString: String =
       user_prefix(session.getUserName) + host + port_suffix(port) +
       (if (session.isConnected) "" else " (disconnected)")
@@ -488,6 +491,7 @@
     def close(): Unit = ()
 
     def hg_url: String = ""
+    def rsync_url: String = ""
 
     def expand_path(path: Path): Path = path.expand
     def bash_path(path: Path): String = File.bash_path(path)

--- a/src/Pure/System/isabelle_tool.scala	Sun May 29 13:06:30 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sun May 29 13:13:45 2022 +0200
@@ -182,7 +182,8 @@
   Dump.isabelle_tool,
   Export.isabelle_tool,
   ML_Process.isabelle_tool,
-  Mercurial.isabelle_tool,
+  Mercurial.isabelle_tool1,
+  Mercurial.isabelle_tool2,
   Mkroot.isabelle_tool,
   Logo.isabelle_tool,
   Options.isabelle_tool,