--- a/etc/build.props Mon Jun 06 19:39:21 2022 +0200
+++ b/etc/build.props Tue Jun 07 12:32:53 2022 +0200
@@ -83,6 +83,7 @@
src/Pure/General/pretty.scala \
src/Pure/General/properties.scala \
src/Pure/General/rdf.scala \
+ src/Pure/General/rsync.scala \
src/Pure/General/scan.scala \
src/Pure/General/sha1.scala \
src/Pure/General/sql.scala \
--- a/src/Pure/Admin/sync_repos.scala Mon Jun 06 19:39:21 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala Tue Jun 07 12:32:53 2022 +0200
@@ -38,7 +38,7 @@
for (hg <- afp_hg) {
progress.echo_if(verbose, "\n* AFP repository:")
- sync(hg, Isabelle_System.rsync_dir(target) + "/AFP", afp_rev)
+ sync(hg, Rsync.rsync_dir(target) + "/AFP", afp_rev)
}
}
--- a/src/Pure/General/mercurial.scala Mon Jun 06 19:39:21 2022 +0200
+++ b/src/Pure/General/mercurial.scala Tue Jun 07 12:32:53 2022 +0200
@@ -306,11 +306,11 @@
require(ssh == SSH.Local, "local repository required")
Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
- Isabelle_System.rsync_init(target, port = port)
+ Rsync.rsync_init(target, port = port)
val list =
- Isabelle_System.rsync(port = port, list = true,
- args = List("--", Isabelle_System.rsync_dir(target))
+ Rsync.rsync(port = port, list = true,
+ args = List("--", Rsync.rsync_dir(target))
).check.out_lines.filterNot(_.endsWith(" ."))
if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
error("No .hg_sync meta data in " + quote(target))
@@ -322,7 +322,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 ""
- Isabelle_System.rsync_init(target, port = port,
+ Rsync.rsync_init(target, port = port,
contents =
File.Content(Hg_Sync.PATH_ID, id_content) ::
File.Content(Hg_Sync.PATH_LOG, log_content) ::
@@ -348,14 +348,14 @@
val protect =
(Hg_Sync.PATH :: contents.map(_.path))
.map(path => "protect /" + File.standard_path(path))
- Isabelle_System.rsync(
+ Rsync.rsync(
progress = progress, port = port, verbose = verbose, thorough = thorough,
dry_run = dry_run,
clean = true,
prune_empty_dirs = true,
filter = protect ::: filter,
args = List("--exclude-from=" + exclude_path.implode, "--",
- Isabelle_System.rsync_dir(source), target)
+ Rsync.rsync_dir(source), target)
).check
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/rsync.scala Tue Jun 07 12:32:53 2022 +0200
@@ -0,0 +1,52 @@
+/* Title: Pure/General/rsync.scala
+ Author: Makarius
+
+Support for rsync: see also https://rsync.samba.org
+*/
+
+package isabelle
+
+
+object Rsync {
+ def rsync(
+ progress: Progress = new Progress,
+ port: Int = SSH.default_port,
+ verbose: Boolean = false,
+ thorough: Boolean = false,
+ prune_empty_dirs: Boolean = false,
+ dry_run: Boolean = false,
+ clean: Boolean = false,
+ list: Boolean = false,
+ filter: List[String] = Nil,
+ args: List[String] = Nil
+ ): Process_Result = {
+ val script =
+ "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
+ (if (verbose) " --verbose" else "") +
+ (if (thorough) " --ignore-times" else " --omit-dir-times") +
+ (if (prune_empty_dirs) " --prune-empty-dirs" else "") +
+ (if (dry_run) " --dry-run" else "") +
+ (if (clean) " --delete-excluded" else "") +
+ (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)
+ }
+
+ def rsync_dir(target: String): String = {
+ if (target.endsWith(":.") || target.endsWith("/.")) target
+ else if (target.endsWith(":") || target.endsWith("/")) target + "."
+ else target + "/."
+ }
+
+ def rsync_init(target: String,
+ port: Int = SSH.default_port,
+ 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,
+ args = List(File.bash_path(init_dir) + "/.", target)).check
+ }
+}
--- a/src/Pure/System/isabelle_system.scala Mon Jun 06 19:39:21 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Jun 07 12:32:53 2022 +0200
@@ -420,48 +420,6 @@
else error("Expected to find GNU tar executable")
}
- def rsync(
- progress: Progress = new Progress,
- port: Int = SSH.default_port,
- verbose: Boolean = false,
- thorough: Boolean = false,
- prune_empty_dirs: Boolean = false,
- dry_run: Boolean = false,
- clean: Boolean = false,
- list: Boolean = false,
- filter: List[String] = Nil,
- args: List[String] = Nil
- ): Process_Result = {
- val script =
- "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
- (if (verbose) " --verbose" else "") +
- (if (thorough) " --ignore-times" else " --omit-dir-times") +
- (if (prune_empty_dirs) " --prune-empty-dirs" else "") +
- (if (dry_run) " --dry-run" else "") +
- (if (clean) " --delete-excluded" else "") +
- (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)
- }
-
- def rsync_dir(target: String): String = {
- if (target.endsWith(":.") || target.endsWith("/.")) target
- else if (target.endsWith(":") || target.endsWith("/")) target + "."
- else target + "/."
- }
-
- def rsync_init(target: String,
- port: Int = SSH.default_port,
- contents: List[File.Content] = Nil
- ): Unit =
- with_tmp_dir("sync") { tmp_dir =>
- val init_dir = make_directory(tmp_dir + Path.explode("init"))
- contents.foreach(_.write(init_dir))
- rsync(port = port, thorough = true,
- args = List(File.bash_path(init_dir) + "/.", target)).check
- }
-
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
with_tmp_file("patch") { patch =>
Isabelle_System.bash(