src/Pure/General/url.scala

--- 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
 }