# HG changeset patch
# User wenzelm
# Date 1654597973 -7200
# Node ID 0dcaf0e5107b81dc5d276d608b59d19fe877a88b
# Parent  65ecf4c5b86893e0cc1f3ff3bbd59671142398b0
clarified modules;

diff -r 65ecf4c5b868 -r 0dcaf0e5107b etc/build.props
--- 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 \
diff -r 65ecf4c5b868 -r 0dcaf0e5107b src/Pure/Admin/sync_repos.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)
     }
   }
 
diff -r 65ecf4c5b868 -r 0dcaf0e5107b src/Pure/General/mercurial.scala
--- 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
       }
     }
diff -r 65ecf4c5b868 -r 0dcaf0e5107b src/Pure/General/rsync.scala
--- /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
+    }
+}
diff -r 65ecf4c5b868 -r 0dcaf0e5107b src/Pure/System/isabelle_system.scala
--- 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(