diff -r 22c41ee13939 -r 8cc1ae43e12e src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Thu Nov 23 11:36:38 2023 +0100
+++ b/src/Pure/General/url.scala	Thu Nov 23 11:40:49 2023 +0100
@@ -31,10 +31,15 @@
 
   /* make and check URLs */
 
-  def apply(name: String): URL = {
-    try { new URL(name) }
-    catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
-  }
+  def apply(name: String): URL =
+    try { new URI(name).toURL }
+    catch {
+      case _: MalformedURLException | _: URISyntaxException =>
+        error("Malformed URL " + quote(name))
+    }
+
+  def resolve(url: URL, route: String): URL =
+    if (route.isEmpty) url else url.toURI.resolve(route).toURL
 
   def is_wellformed(name: String): Boolean =
     try { Url(name); true }