src/Pure/Admin/sync_repos.scala

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