--- a/src/Pure/Admin/build_history.scala Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/Admin/build_history.scala Tue Jun 07 17:07:10 2022 +0200
@@ -534,7 +534,8 @@
def sync_repos(target: Path, accurate: Boolean = false,
rev: String = "", afp_rev: String = "", afp: Boolean = false
): Unit = {
- Sync_Repos.sync_repos(ssh.rsync_path(target), port = ssh.port, progress = progress,
+ val context = Rsync.Context(progress, port = ssh.port)
+ Sync_Repos.sync_repos(context, ssh.rsync_path(target),
thorough = accurate, preserve_jars = !accurate,
rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
}
--- a/src/Pure/Admin/sync_repos.scala Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala Tue Jun 07 17:07:10 2022 +0200
@@ -8,9 +8,7 @@
object Sync_Repos {
- def sync_repos(target: String,
- progress: Progress = new Progress,
- port: Int = SSH.default_port,
+ def sync_repos(context: Rsync.Context, target: String,
verbose: Boolean = false,
thorough: Boolean = false,
preserve_jars: Boolean = false,
@@ -27,17 +25,17 @@
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)
+ hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run,
+ contents = contents, filter = filter ::: more_filter)
}
- progress.echo_if(verbose, "\n* Isabelle repository:")
+ context.progress.echo_if(verbose, "\n* Isabelle repository:")
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_if(verbose, "\n* AFP repository:")
+ context.progress.echo_if(verbose, "\n* AFP repository:")
sync(hg, Rsync.append(target, "AFP"), afp_rev)
}
}
@@ -94,7 +92,8 @@
}
val progress = new Console_Progress
- sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
+ val context = Rsync.Context(progress, port = port)
+ sync_repos(context, target, verbose = verbose, thorough = thorough,
preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
afp_rev = afp_rev)
}
--- a/src/Pure/General/mercurial.scala Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/General/mercurial.scala Tue Jun 07 17:07:10 2022 +0200
@@ -293,9 +293,7 @@
def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
- def sync(target: String,
- progress: Progress = new Progress,
- port: Int = SSH.default_port,
+ def sync(context: Rsync.Context, target: String,
verbose: Boolean = false,
thorough: Boolean = false,
dry_run: Boolean = false,
@@ -306,10 +304,10 @@
require(ssh == SSH.Local, "local repository required")
Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
- Rsync.rsync_init(target, port = port)
+ Rsync.rsync_init(context, target)
val list =
- Rsync.rsync(port = port, list = true,
+ Rsync.rsync(context, list = true,
args = List("--", Rsync.terminate(target))
).check.out_lines.filterNot(_.endsWith(" ."))
if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
@@ -322,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(target, port = port,
+ Rsync.rsync_init(context, target,
contents =
File.Content(Hg_Sync.PATH_ID, id_content) ::
File.Content(Hg_Sync.PATH_LOG, log_content) ::
@@ -348,8 +346,9 @@
val protect =
(Hg_Sync.PATH :: contents.map(_.path))
.map(path => "protect /" + File.standard_path(path))
- Rsync.rsync(
- progress = progress, port = port, verbose = verbose, thorough = thorough,
+ Rsync.rsync(context,
+ verbose = verbose,
+ thorough = thorough,
dry_run = dry_run,
clean = true,
prune_empty_dirs = true,
@@ -606,7 +605,8 @@
case Some(dir) => repository(dir)
case None => the_repository(Path.current)
}
- hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
+ val context = Rsync.Context(progress, port = port)
+ hg.sync(context, target, verbose = verbose, thorough = thorough,
dry_run = dry_run, filter = filter, rev = rev)
}
)
--- a/src/Pure/General/rsync.scala Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/General/rsync.scala Tue Jun 07 17:07:10 2022 +0200
@@ -8,9 +8,13 @@
object Rsync {
+ sealed case class Context(progress: Progress, port: Int = SSH.default_port) {
+ def command: String =
+ "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port)
+ }
+
def rsync(
- progress: Progress = new Progress,
- port: Int = SSH.default_port,
+ context: Context,
verbose: Boolean = false,
thorough: Boolean = false,
prune_empty_dirs: Boolean = false,
@@ -21,7 +25,7 @@
args: List[String] = Nil
): Process_Result = {
val script =
- "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
+ context.command +
(if (verbose) " --verbose" else "") +
(if (thorough) " --ignore-times" else " --omit-dir-times") +
(if (prune_empty_dirs) " --prune-empty-dirs" else "") +
@@ -30,17 +34,16 @@
(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, echo = true)
+ context.progress.bash(script, echo = true)
}
- def rsync_init(target: String,
- port: Int = SSH.default_port,
+ def rsync_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(port = port, thorough = true,
+ rsync(context, thorough = true,
args = List(File.bash_path(init_dir) + "/.", target)).check
}