provide .hg_sync meta data;
always clean target, but guard it wrt. .hg_sync for robustness (no need for dry-run);
updated and clarified documentation;

--- a/src/Doc/System/Misc.thy	Sat Jun 04 16:54:24 2022 +0200
+++ b/src/Doc/System/Misc.thy	Sun Jun 05 19:19:55 2022 +0200
@@ -304,20 +304,17 @@
 
 text \<open>
   The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with
-  a target directory, using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close>
-  notation for destinations.
+  a target directory.
 
   @{verbatim [display]
 \<open>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: 22)
@@ -327,21 +324,21 @@
   which can be local or remote (using notation of rsync).\<close>}
 
   The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh),
-  using \<^verbatim>\<open>rsync\<close> notation (see examples below). The content is written
-  directly into the target, \<^emph>\<open>without\<close> creating a separate sub-directory.
+  using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close> notation for
+  destinations; see also examples below. The content is written directly into
+  the target, \<^emph>\<open>without\<close> creating a separate sub-directory. The special
+  sub-directory \<^verbatim>\<open>.hg_sync\<close> within the target contains meta data from the
+  original Mercurial repository. Repeated synchronization is guarded by the
+  presence of a \<^verbatim>\<open>.hg_sync\<close> sub-directory: this sanity check prevents
+  accidental changes (or deletion!) of targets that were not created by @{tool
+  hg_sync}.
 
   \<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default
   is the current state of the working directory (which might be uncommitted).
 
   \<^medskip> Option \<^verbatim>\<open>-v\<close> enables verbose mode. Option \<^verbatim>\<open>-n\<close> enables ``dry-run'' mode:
-  operations are only simulated and printed as in verbose mode. Option \<^verbatim>\<open>-f\<close>
-  disables ``dry-run'' mode and thus forces changes to be applied.
-
-  \<^medskip> Option \<^verbatim>\<open>-C\<close> causes deletion of all unknown/ignored files on the target.
-  This is potentially dangerous: giving a wrong target directory will cause
-  its total destruction! For robustness, option \<^verbatim>\<open>-C\<close> implies option \<^verbatim>\<open>-n\<close>,
-  for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\<open>-f\<close> is required
-  to force actual deletions on the target.
+  operations are only simulated; use it with option \<^verbatim>\<open>-v\<close> to actually see
+  results.
 
   \<^medskip> Option \<^verbatim>\<open>-F\<close> adds a filter rule to the underlying \<^verbatim>\<open>rsync\<close> command;
   multiple \<^verbatim>\<open>-F\<close> options may be given to accumulate a list of rules.
@@ -363,10 +360,7 @@
 text \<open>
   Synchronize the current repository onto a remote host, with accurate
   treatment of all content:
-  @{verbatim [display] \<open>  isabelle hg_sync -T -C remotename:test/repos\<close>}
-
-  So far, this is only a dry run. In a realistic situation, it requires
-  consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
+  @{verbatim [display] \<open>  isabelle hg_sync -T remotename:test/repos\<close>}
 \<close>
 
 

--- a/src/Pure/Admin/sync_repos.scala	Sat Jun 04 16:54:24 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Sun Jun 05 19:19:55 2022 +0200
@@ -15,38 +15,30 @@
     thorough: Boolean = false,
     preserve_jars: Boolean = false,
     dry_run: Boolean = false,
-    clean: Boolean = false,
     rev: String = "",
     afp_root: Option[Path] = None,
     afp_rev: String = ""
   ): Unit = {
-    val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/"
-
     val hg = Mercurial.self_repository()
     val afp_hg = afp_root.map(Mercurial.repository(_))
 
     val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
 
-    def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit =
-      hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose || dry_run,
-        thorough = thorough, dry_run = dry_run, clean = clean, filter = filter ::: more_filter)
+    def sync(hg: Mercurial.Repository, dest: String, r: String,
+      contents: List[File.Content] = Nil, filter: List[String] = Nil
+    ): Unit = {
+      hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose,
+        thorough = thorough, dry_run = dry_run, contents = contents, filter = filter ::: more_filter)
+    }
 
     progress.echo("\n* Isabelle repository:")
-    sync(hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID"))
-
-    if (!dry_run) {
-      Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
-        val id_path = tmp_dir + Path.explode("ISABELLE_ID")
-        File.write(id_path, hg.id(rev = rev))
-        Isabelle_System.rsync(port = port, thorough = thorough,
-          args = List(File.standard_path(id_path), target_dir + "etc/")
-        ).check
-      }
-    }
+    sync(hg, target, rev,
+      contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
+      filter = List("protect /AFP"))
 
     for (hg <- afp_hg) {
       progress.echo("\n* AFP repository:")
-      sync(hg, target_dir + "AFP", afp_rev)
+      sync(hg, Isabelle_System.rsync_dir(target) + "/AFP", afp_rev)
     }
   }
 
@@ -54,7 +46,6 @@
     Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
       Scala_Project.here, { args =>
         var afp_root: Option[Path] = None
-        var clean = false
         var preserve_jars = false
         var thorough = false
         var afp_rev = ""
@@ -69,11 +60,8 @@
   Options are:
     -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
     -J           preserve *.jar files
-    -C           clean all unknown/ignored files on target
-                 (implies -n for testing; use option -f to confirm)
     -T           thorough treatment of file content and directory times
     -a REV       explicit AFP revision (default: state of working directory)
-    -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 + """)
@@ -81,22 +69,18 @@
 
   Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
 
-  Examples (without -f as "dry-run"):
+  Example: quick testing
 
-   * quick testing
+    isabelle sync_repos -A: -J testmachine:test/isabelle_afp
 
-      isabelle sync_repos -A: -J -C testmachine:test/isabelle_afp
+  Example: accurate testing
 
-   * accurate testing
-
-      isabelle sync_repos -A: -T -C testmachine:test/isabelle_afp
+    isabelle sync_repos -A: -T testmachine:test/isabelle_afp
 """,
           "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
           "J" -> (_ => preserve_jars = true),
-          "C" -> { _ => clean = true; dry_run = true },
           "T" -> (_ => thorough = true),
           "a:" -> (arg => afp_rev = arg),
-          "f" -> (_ => dry_run = false),
           "n" -> (_ => dry_run = true),
           "r:" -> (arg => rev = arg),
           "p:" -> (arg => port = Value.Int.parse(arg)),
@@ -111,8 +95,8 @@
 
         val progress = new Console_Progress
         sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
-          preserve_jars = preserve_jars, dry_run = dry_run, clean = clean, rev = rev,
-          afp_root = afp_root, afp_rev = afp_rev)
+          preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
+          afp_rev = afp_rev)
       }
     )
 }

--- 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)
       }
     )
 }

--- a/src/Pure/System/isabelle_system.scala	Sat Jun 04 16:54:24 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Jun 05 19:19:55 2022 +0200
@@ -426,8 +426,10 @@
     port: Int = SSH.default_port,
     verbose: Boolean = false,
     thorough: Boolean = false,
+    prune_empty_dirs: Boolean = false,
     dry_run: Boolean = false,
     clean: Boolean = false,
+    list: Boolean = false,
     filter: List[String] = Nil,
     args: List[String] = Nil
   ): Process_Result = {
@@ -435,13 +437,32 @@
       "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
         (if (verbose) " --verbose" else "") +
         (if (thorough) " --ignore-times" else " --omit-dir-times") +
+        (if (prune_empty_dirs) " --prune-empty-dirs" else "") +
         (if (dry_run) " --dry-run" else "") +
         (if (clean) " --delete-excluded" else "") +
+        (if (list) " --list-only --no-human-readable" else "") +
         filter.map(s => " --filter=" + Bash.string(s)).mkString +
         (if (args.nonEmpty) " " + Bash.strings(args) else "")
     progress.bash(script, cwd = cwd, echo = true)
   }
 
+  def rsync_dir(target: String): String = {
+    if (target.endsWith(":.") || target.endsWith("/.")) target
+    else if (target.endsWith(":") || target.endsWith("/")) target + "."
+    else target + "/."
+  }
+
+  def rsync_init(target: String,
+    port: Int = SSH.default_port,
+    contents: List[File.Content] = Nil
+  ): Unit =
+    with_tmp_dir("sync") { tmp_dir =>
+      val init_dir = make_directory(tmp_dir + Path.explode("init"))
+      contents.foreach(_.write(init_dir))
+      rsync(port = port, thorough = true,
+        args = List(File.bash_path(init_dir) + "/.", target)).check
+    }
+
   def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
     with_tmp_file("patch") { patch =>
       Isabelle_System.bash(