src/Pure/System/isabelle_system.scala

--- a/src/Pure/System/isabelle_system.scala	Sat Jun 04 16:54:24 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Jun 05 19:19:55 2022 +0200
@@ -426,8 +426,10 @@
     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 = {
@@ -435,13 +437,32 @@
       "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, cwd = cwd, 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(