more direct hg_sync init via ssh (see also 721b3278c8e4);

--- a/src/Pure/General/file.scala	Fri Apr 14 22:19:28 2023 +0200
+++ b/src/Pure/General/file.scala	Fri Apr 14 22:55:01 2023 +0200
@@ -383,10 +383,10 @@
   final class Content private[File](val path: Path, val content: Bytes) {
     override def toString: String = path.toString
 
-    def write(dir: Path): Unit = {
+    def write(dir: Path, ssh: SSH.System = SSH.Local): Unit = {
       val full_path = dir + path
-      Isabelle_System.make_directory(full_path.expand.dir)
-      Bytes.write(full_path, content)
+      ssh.make_directory(ssh.expand_path(full_path).dir)
+      ssh.write_bytes(full_path, content)
     }
   }
 

--- a/src/Pure/General/mercurial.scala	Fri Apr 14 22:19:28 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Fri Apr 14 22:55:01 2023 +0200
@@ -307,20 +307,19 @@
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
         Hg_Sync.check_directory(target, ssh = context.ssh)
 
-        Rsync.init(context.no_progress, target)
-
         val id_content = id(rev = rev)
         val is_changed = id_content.endsWith("+")
         val log_content = if (is_changed) "" else log(rev = rev, options = "-l1")
         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.init(context.no_progress, target,
-          contents =
-            File.content(Hg_Sync.PATH_ID, id_content) ::
-            File.content(Hg_Sync.PATH_LOG, log_content) ::
-            File.content(Hg_Sync.PATH_DIFF, diff_content) ::
-            File.content(Hg_Sync.PATH_STAT, stat_content) :: contents)
+        val all_contents =
+          File.content(Hg_Sync.PATH_ID, id_content) ::
+          File.content(Hg_Sync.PATH_LOG, log_content) ::
+          File.content(Hg_Sync.PATH_DIFF, diff_content) ::
+          File.content(Hg_Sync.PATH_STAT, stat_content) :: contents
+
+        all_contents.foreach(_.write(target, ssh = context.ssh))
 
         val (exclude, source) =
           if (rev.isEmpty) {

--- a/src/Pure/General/rsync.scala	Fri Apr 14 22:19:28 2023 +0200
+++ b/src/Pure/General/rsync.scala	Fri Apr 14 22:55:01 2023 +0200
@@ -28,9 +28,6 @@
   ) {
     override def toString: String = directory.toString
 
-    def no_progress: Context = new Context(directory, new Progress, archive, stats)
-    def no_archive: Context = new Context(directory, progress, false, stats)
-
     def ssh: SSH.System = directory.ssh
 
     def command: String = {
@@ -70,17 +67,4 @@
         if_proper(args, " " + Bash.strings(args))
     progress.bash(script, echo = true)
   }
-
-  def init(context: Context, target: Path,
-    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))
-      exec(context.no_archive,
-        thorough = true,
-        args =
-          List(if (contents.nonEmpty) "--archive" else "--dirs",
-            File.bash_path(init_dir) + "/.", context.target(target))).check
-    }
 }