tuned signature;
authorwenzelm
Tue, 07 Jun 2022 17:10:51 +0200
changeset 75526 57b6a28e4eba
parent 75525 68162e4f60a7
child 75527 a66fd84a30b7
tuned signature;
src/Pure/General/mercurial.scala
src/Pure/General/rsync.scala
--- a/src/Pure/General/mercurial.scala	Tue Jun 07 17:07:10 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Jun 07 17:10:51 2022 +0200
@@ -304,10 +304,10 @@
       require(ssh == SSH.Local, "local repository required")
 
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
-        Rsync.rsync_init(context, target)
+        Rsync.init(context, target)
 
         val list =
-          Rsync.rsync(context, list = true,
+          Rsync.exec(context, list = true,
             args = List("--", Rsync.terminate(target))
           ).check.out_lines.filterNot(_.endsWith(" ."))
         if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
@@ -320,7 +320,7 @@
         val diff_content = if (is_changed) diff(rev = rev, options = "--git") else ""
         val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else ""
 
-        Rsync.rsync_init(context, target,
+        Rsync.init(context, target,
           contents =
             File.Content(Hg_Sync.PATH_ID, id_content) ::
             File.Content(Hg_Sync.PATH_LOG, log_content) ::
@@ -346,7 +346,7 @@
         val protect =
           (Hg_Sync.PATH :: contents.map(_.path))
             .map(path => "protect /" + File.standard_path(path))
-        Rsync.rsync(context,
+        Rsync.exec(context,
           verbose = verbose,
           thorough = thorough,
           dry_run = dry_run,
--- a/src/Pure/General/rsync.scala	Tue Jun 07 17:07:10 2022 +0200
+++ b/src/Pure/General/rsync.scala	Tue Jun 07 17:10:51 2022 +0200
@@ -13,7 +13,7 @@
       "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port)
   }
 
-  def rsync(
+  def exec(
     context: Context,
     verbose: Boolean = false,
     thorough: Boolean = false,
@@ -37,13 +37,13 @@
     context.progress.bash(script, echo = true)
   }
 
-  def rsync_init(context: Context, target: String,
+  def init(context: Context, target: String,
     contents: List[File.Content] = Nil
   ): Unit =
     Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
       val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init"))
       contents.foreach(_.write(init_dir))
-      rsync(context, thorough = true,
+      exec(context, thorough = true,
         args = List(File.bash_path(init_dir) + "/.", target)).check
     }