recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL);
--- 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()
}