src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Mon Jan 22 14:40:30 2024 +0100
+++ b/src/Pure/General/url.scala	Mon Jan 22 22:18:20 2024 +0100
@@ -39,14 +39,11 @@
 
   def apply(uri: URI): Url = new Url(uri)
 
-  def apply(name: String): Url = {
-    val uri =
-      try { new URI(name) }
-      catch {
-        case exn: Throwable if is_malformed(exn) => error("Malformed URL " + quote(name))
-      }
-    Url(uri)
-  }
+  def apply(name: String): Url =
+    try { new Url(new URI(name)) }
+    catch {
+      case exn: Throwable if is_malformed(exn) => error("Malformed URL " + quote(name))
+    }
 
   def is_wellformed(name: String): Boolean =
     try { Url(name); true }
@@ -163,7 +160,7 @@
   def resolve(route: String): Url =
     if (route.isEmpty) this else new Url(uri.resolve(route))
 
-  def java_url: java.net.URL = uri.toURL
+  val java_url: java.net.URL = uri.toURL
   def open_stream(): InputStream = java_url.openStream()
   def open_connection(): URLConnection = java_url.openConnection()
 }