clarified signature;

--- a/src/Pure/General/mercurial.scala	Sun Dec 11 11:47:28 2022 +0100
+++ b/src/Pure/General/mercurial.scala	Sun Dec 11 12:52:46 2022 +0100
@@ -309,7 +309,7 @@
         Rsync.init(context0, target)
 
         val list =
-          Rsync.exec(context0, list = true, args = List("--", Rsync.direct(target)))
+          Rsync.exec(context0, list = true, args = List("--", Url.direct_path(target)))
             .check.out_lines.filterNot(_.endsWith(" ."))
         if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
           error("No .hg_sync meta data in " + quote(target))
@@ -355,7 +355,7 @@
           prune_empty_dirs = true,
           filter = protect ::: filter,
           args = List("--exclude-from=" + exclude_path.implode, "--",
-            Rsync.direct(source), target)
+            Url.direct_path(source), target)
         ).check
       }
     }

--- a/src/Pure/General/rsync.scala	Sun Dec 11 11:47:28 2022 +0100
+++ b/src/Pure/General/rsync.scala	Sun Dec 11 12:52:46 2022 +0100
@@ -58,13 +58,4 @@
           List(if (contents.nonEmpty) "--archive" else "--dirs",
             File.bash_path(init_dir) + "/.", target)).check
     }
-
-  def direct(prefix: String): String =
-    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "."
-    else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix
-    else prefix + "/."
-
-  def append(prefix: String, suffix: String): String =
-    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix
-    else prefix + "/" + suffix
 }

--- a/src/Pure/General/url.scala	Sun Dec 11 11:47:28 2022 +0100
+++ b/src/Pure/General/url.scala	Sun Dec 11 12:52:46 2022 +0100
@@ -100,4 +100,16 @@
 
   def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
+
+
+  /* generic path notation: local, ssh, rsync, http */
+
+  def direct_path(prefix: String): String =
+    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "."
+    else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix
+    else prefix + "/."
+
+  def append_path(prefix: String, suffix: String): String =
+    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix
+    else prefix + "/" + suffix
 }

--- a/src/Pure/Tools/sync.scala	Sun Dec 11 11:47:28 2022 +0100
+++ b/src/Pure/Tools/sync.scala	Sun Dec 11 12:52:46 2022 +0100
@@ -64,7 +64,7 @@
 
     for (hg <- afp_hg) {
       context.progress.echo_if(verbose, "\n* AFP repository:")
-      sync(hg, Rsync.append(target, "AFP"), afp_rev)
+      sync(hg, Url.append_path(target, "AFP"), afp_rev)
     }
 
     val images =
@@ -72,8 +72,9 @@
         dirs = afp_root.map(_ + Path.explode("thys")).toList)
     if (images.nonEmpty) {
       context.progress.echo_if(verbose, "\n* Session images:")
+      val heaps = Url.append_path(target, "heaps/")
       Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run,
-        args = List("--relative", "--") ::: images ::: List(Rsync.append(target, "heaps/"))).check
+        args = List("--relative", "--") ::: images ::: List(heaps)).check
     }
   }