# HG changeset patch
# User wenzelm
# Date 1716564709 -7200
# Node ID c934f0e51f1c516968008a4047383274ae31e1a8
# Parent  9f3e0d98fbec3c757479fbe252bb56f7073f99de
tuned names;

diff -r 9f3e0d98fbec -r c934f0e51f1c src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Fri May 24 17:14:02 2024 +0200
+++ b/src/Pure/Tools/sync.scala	Fri May 24 17:31:49 2024 +0200
@@ -46,27 +46,27 @@
   ): Unit = {
     val progress = context.progress
 
-    val hg = Mercurial.self_repository()
-    val afp_hg = afp_root.map(Mercurial.repository(_))
+    val self = Mercurial.self_repository()
+    val afp = afp_root.map(Mercurial.repository(_))
 
     val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
 
-    def hg_sync(hg: Mercurial.Repository, dest: Path, r: String,
+    def synchronize(src: Mercurial.Repository, dest: Path, r: String,
       contents: List[File.Content] = Nil, filter: List[String] = Nil
     ): Unit = {
-      hg.sync(context, dest, rev = r, thorough = thorough, dry_run = dry_run,
+      src.sync(context, dest, rev = r, thorough = thorough, dry_run = dry_run,
         contents = contents, filter = filter ::: more_filter)
     }
 
-    progress.echo("\n* Isabelle repository:", verbose = true)
+    progress.echo("\n* Isabelle:", verbose = true)
     val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
-    hg_sync(hg, target, rev,
-      contents = List(File.content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
+    synchronize(self, target, rev,
+      contents = List(File.content(Path.explode("etc/ISABELLE_ID"), self.id(rev = rev))),
       filter = filter_heaps ::: List("protect /AFP"))
 
-    for (hg <- afp_hg) {
-      progress.echo("\n* AFP repository:", verbose = true)
-      hg_sync(hg, target + Path.explode("AFP"), afp_rev)
+    for (src <- afp) {
+      progress.echo("\n* AFP:", verbose = true)
+      synchronize(src, target + Path.explode("AFP"), afp_rev)
     }
 
     val images =