# HG changeset patch
# User wenzelm
# Date 1700736049 -3600
# Node ID 8cc1ae43e12e37a48fd3d43c0229930f1655dab1
# Parent  22c41ee13939fd147708ba4c716687855831abfb
clarified signature: avoid deprecated URL constructors;

diff -r 22c41ee13939 -r 8cc1ae43e12e src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Nov 23 11:36:38 2023 +0100
+++ b/src/Pure/General/file.scala	Thu Nov 23 11:40:49 2023 +0100
@@ -13,7 +13,7 @@
 import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
   FileVisitOption, FileVisitResult}
 import java.nio.file.attribute.{BasicFileAttributes, PosixFilePermission}
-import java.net.{URI, URL, MalformedURLException}
+import java.net.{URI, URL, MalformedURLException, URISyntaxException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.EnumSet
 
@@ -35,12 +35,15 @@
 
   def standard_url(name: String): String =
     try {
-      val url = new URL(name)
-      if (url.getProtocol == "file" && Url.is_wellformed_file(name))
+      val url = new URI(name).toURL
+      if (url.getProtocol == "file" && Url.is_wellformed_file(name)) {
         standard_path(Url.parse_file(name))
+      }
       else name
     }
-    catch { case _: MalformedURLException => standard_path(name) }
+    catch {
+      case _: MalformedURLException | _: URISyntaxException => standard_path(name)
+    }
 
 
   /* platform path (Windows or Posix) */
diff -r 22c41ee13939 -r 8cc1ae43e12e src/Pure/General/json_api.scala
--- a/src/Pure/General/json_api.scala	Thu Nov 23 11:36:38 2023 +0100
+++ b/src/Pure/General/json_api.scala	Thu Nov 23 11:40:49 2023 +0100
@@ -19,7 +19,7 @@
     override def toString: String = url.toString
 
     def get(route: String): HTTP.Content =
-      HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
+      HTTP.Client.get(Url.resolve(url, route))
 
     def get_root(route: String = ""): Root =
       Root(get(if_proper(route, "/" + route)).json)
diff -r 22c41ee13939 -r 8cc1ae43e12e src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Thu Nov 23 11:36:38 2023 +0100
+++ b/src/Pure/General/mailman.scala	Thu Nov 23 11:40:49 2023 +0100
@@ -356,7 +356,7 @@
 
     def list_tag: String = proper_string(tag).getOrElse(list_name)
 
-    def read_text(href: String): String = Url.read(new URL(main_url, href))
+    def read_text(href: String): String = Url.read(Url.resolve(main_url, href))
 
     def hrefs_text: List[String] =
       """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(main_html).map(_.group(1)).toList
@@ -371,7 +371,7 @@
     def get(target_dir: Path, href: String, progress: Progress = new Progress): Option[Path] = {
       val dir = target_dir + Path.basic(list_name)
       val path = dir + Path.explode(href)
-      val url = new URL(main_url, href)
+      val url = Url.resolve(main_url, href)
       val connection = url.openConnection
       try {
         val length = connection.getContentLengthLong
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 }