# HG changeset patch
# User wenzelm
# Date 1680965881 -7200
# Node ID 721b3278c8e47c7eb2b4374dd1e07b8dca3a3383
# Parent  4046731cfa6ceb3d8947d65402d783388c085b44
more direct Hg_Sync.check_directory via SSH operations;

diff -r 4046731cfa6c -r 721b3278c8e4 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Apr 08 16:44:24 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Apr 08 16:58:01 2023 +0200
@@ -126,6 +126,11 @@
     val PATH_DIFF: Path = PATH + Path.explode("diff")
     val PATH_STAT: Path = PATH + Path.explode("stat")
 
+    def check_directory(root: Path, ssh: SSH.System = SSH.Local): Unit =
+      if (ssh.is_dir(root) && !ssh.is_dir(root + PATH) && ssh.read_dir(root).nonEmpty) {
+        error("No .hg_sync meta data in " + ssh.rsync_path(root))
+      }
+
     def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean =
       ssh.is_dir(root + PATH)
 
@@ -303,18 +308,12 @@
       require(ssh.is_local, "local repository required")
 
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
+        Hg_Sync.check_directory(target, ssh = context.ssh)
+
         val context0 = context.copy(progress = new Progress)
 
         Rsync.init(context0, target)
 
-        val list =
-          Rsync.exec(context0, list = true,
-            args = List("--", context.target(target, direct = true)))
-            .check.out_lines.filterNot(_.endsWith(" ."))
-        if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
-          error("No .hg_sync meta data in " + quote(context.target(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")
diff -r 4046731cfa6c -r 721b3278c8e4 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sat Apr 08 16:44:24 2023 +0200
+++ b/src/Pure/General/rsync.scala	Sat Apr 08 16:58:01 2023 +0200
@@ -33,7 +33,6 @@
     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 = {
@@ -45,7 +44,6 @@
         (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_proper(args, " " + Bash.strings(args))
     progress.bash(script, echo = true)