# HG changeset patch
# User wenzelm
# Date 1670762794 -3600
# Node ID aeded421d37449bee2cded50bcfb5c532661ebc4
# Parent  d5adc9126ae8d61ffeef61fe631f088a8d3383a7
clarified signature: more general operations;

diff -r d5adc9126ae8 -r aeded421d374 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Sun Dec 11 12:52:46 2022 +0100
+++ b/src/Pure/General/url.scala	Sun Dec 11 13:46:34 2022 +0100
@@ -102,14 +102,17 @@
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 
 
-  /* generic path notation: local, ssh, rsync, http */
+  /* generic path notation: local, ssh, rsync, ftp, http */
 
   def direct_path(prefix: String): String =
-    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "."
-    else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix
+    if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.isEmpty) prefix + "."
+    else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix == ".") prefix
     else prefix + "/."
 
   def append_path(prefix: String, suffix: String): String =
-    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix
+    if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.isEmpty) prefix + suffix
+    else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix == ".") {
+      prefix.substring(0, prefix.length - 1) + suffix
+    }
     else prefix + "/" + suffix
 }
diff -r d5adc9126ae8 -r aeded421d374 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Dec 11 12:52:46 2022 +0100
+++ b/src/Pure/Thy/html.scala	Sun Dec 11 13:46:34 2022 +0100
@@ -429,10 +429,8 @@
       .mkString("", "\n\n", "\n")
   }
 
-  def fonts_css_dir(prefix: String = ""): String = {
-    val prefix1 = if (prefix.isEmpty || prefix.endsWith("/")) prefix else prefix + "/"
-    fonts_css(fonts_dir(prefix1 + fonts_path.implode))
-  }
+  def fonts_css_dir(prefix: String = ""): String =
+    fonts_css(fonts_dir(Url.append_path(prefix, fonts_path.implode)))
 
 
   /* document directory context (fonts + css) */
diff -r d5adc9126ae8 -r aeded421d374 src/Pure/Tools/flarum.scala
--- a/src/Pure/Tools/flarum.scala	Sun Dec 11 12:52:46 2022 +0100
+++ b/src/Pure/Tools/flarum.scala	Sun Dec 11 13:46:34 2022 +0100
@@ -17,9 +17,7 @@
   def server(url: URL): Server = new Server(url)
 
   class Server private[Flarum](url: URL) extends JSON_API.Service(url) {
-    def get_api(route: String): JSON_API.Root =
-      get_root("api" + (if (route.isEmpty) "" else "/" + route))
-
+    def get_api(route: String): JSON_API.Root = get_root(Url.append_path("api", route))
     val root: JSON_API.Root = get_api("")
     def users: JSON_API.Root = get_api("users")
     def groups: JSON_API.Root = get_api("groups")