tuned names;
authorwenzelm
Fri, 24 May 2024 17:31:49 +0200
changeset 80191 c934f0e51f1c
parent 80190 9f3e0d98fbec
child 80192 36e6ba1527f0
tuned names;
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 =