diff -r 0106c89fb71f -r b32fdb67f851 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Jun 04 16:54:24 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sun Jun 05 19:19:55 2022 +0200
@@ -115,6 +115,12 @@
     archive_info(root).map(info => info.tags.mkString(" "))
 
 
+  /* hg_sync meta data */
+
+  val HG_SYNC: Path = Path.explode(".hg_sync")
+  val HG_SYNC_ID: Path = HG_SYNC + Path.explode("id")
+
+
   /* repository access */
 
   def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
@@ -262,13 +268,26 @@
       verbose: Boolean = false,
       thorough: Boolean = false,
       dry_run: Boolean = false,
-      clean: Boolean = false,
       filter: List[String] = Nil,
+      contents: List[File.Content] = Nil,
       rev: String = ""
     ): Unit = {
       require(ssh == SSH.Local, "local repository required")
 
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
+        Isabelle_System.rsync_init(target, port = port)
+
+        val list =
+          Isabelle_System.rsync(port = port, list = true,
+            args = List("--", Isabelle_System.rsync_dir(target))
+          ).check.out_lines.filterNot(_.endsWith(" ."))
+        if (list.nonEmpty && !list.exists(_.endsWith(" .hg_sync"))) {
+          error("No .hg_sync meta data in " + quote(target))
+        }
+
+        Isabelle_System.rsync_init(target, port = port,
+          contents = File.Content(HG_SYNC_ID, id(rev = rev)) :: contents)
+
         val (options, source) =
           if (rev.isEmpty) {
             val exclude_path = tmp_dir + Path.explode("exclude")
@@ -284,10 +303,16 @@
             archive(source, rev = rev)
             (Nil, source)
           }
+
+        val protect =
+          (HG_SYNC :: contents.map(_.path)).map(path => "protect /" + File.standard_path(path))
         Isabelle_System.rsync(
           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)
+          dry_run = dry_run,
+          clean = true,
+          prune_empty_dirs = true,
+          filter = protect ::: filter,
+          args = options ::: List("--", Isabelle_System.rsync_dir(source), target)
         ).check
       }
     }
@@ -492,7 +517,6 @@
   val isabelle_tool2 =
     Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
       Scala_Project.here, { args =>
-        var clean = false
         var filter: List[String] = Nil
         var root: Option[Path] = None
         var thorough = false
@@ -505,13 +529,11 @@
 Usage: isabelle hg_sync [OPTIONS] TARGET
 
   Options are:
-    -C           clean all unknown/ignored files on target
-                 (implies -n for testing; use option -f to confirm)
-    -F RULE      add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
+    -F RULE      add rsync filter RULE
+                 (e.g. "protect /foo" to avoid deletion)
     -R ROOT      explicit repository root directory
                  (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 + """)
@@ -520,11 +542,9 @@
   Synchronize Mercurial repository with TARGET directory,
   which can be local or remote (using notation of rsync).
 """,
-          "C" -> { _ => clean = true; dry_run = true },
           "F:" -> (arg => filter = filter ::: List(arg)),
           "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)),
@@ -543,8 +563,8 @@
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        hg.sync(target, progress = progress, port = port, verbose = verbose || dry_run,
-          thorough = thorough, dry_run = dry_run, clean = clean, filter = filter, rev = rev)
+        hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
+          dry_run = dry_run, filter = filter, rev = rev)
       }
     )
 }