clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);

--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -8,16 +8,14 @@
 
 import isabelle._
 
-import java.net.URL
-
 
 object SystemOnTPTP {
   /* requests */
 
-  def get_url(options: Options): URL = Url(options.string("SystemOnTPTP"))
+  def get_url(options: Options): Url = Url(options.string("SystemOnTPTP"))
 
   def post_request(
-    url: URL,
+    url: Url,
     parameters: List[(String, Any)],
     timeout: Time = HTTP.Client.default_timeout
   ): HTTP.Content = {
@@ -33,7 +31,7 @@
 
   /* list systems */
 
-  def list_systems(url: URL): HTTP.Content =
+  def list_systems(url: Url): HTTP.Content =
     post_request(url,
       List("SubmitButton" -> "ListSystems",
         "ListStatus" -> "READY",
@@ -47,7 +45,7 @@
 
   /* run system */
 
-  def run_system(url: URL,
+  def run_system(url: Url,
     system: String,
     problem: String,
     extra: String = "",

--- a/src/Pure/General/bytes.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/General/bytes.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -69,7 +69,7 @@
       new Bytes(out.toByteArray, 0, out.size)
     }
 
-  def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
+  def read_url(name: String): Bytes = using(Url(name).open_stream())(read_stream(_))
 
   def read_file(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
     val length = File.size(path)

--- a/src/Pure/General/http.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/General/http.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -63,11 +63,11 @@
     val default_timeout: Time = Time.seconds(180)
 
     def open_connection(
-      url: URL,
+      url: Url,
       timeout: Time = default_timeout,
       user_agent: String = ""
     ): HttpURLConnection = {
-      url.openConnection match {
+      url.open_connection() match {
         case connection: HttpURLConnection =>
           if (0 < timeout.ms && timeout.ms <= Int.MaxValue) {
             val ms = timeout.ms.toInt
@@ -88,7 +88,7 @@
         val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
         val stop = Time.now()
 
-        val file_name = Url.file_name(connection.getURL)
+        val file_name = Url.file_name(Url(connection.getURL.toURI))
         val mime_type = Option(connection.getContentType).getOrElse(Content.default_mime_type)
         val encoding =
           (connection.getContentEncoding, mime_type) match {
@@ -101,11 +101,11 @@
       }
     }
 
-    def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
+    def get(url: Url, timeout: Time = default_timeout, user_agent: String = ""): Content =
       get_content(open_connection(url, timeout = timeout, user_agent = user_agent))
 
     def post(
-      url: URL,
+      url: Url,
       parameters: List[(String, Any)],
       timeout: Time = default_timeout,
       user_agent: String = ""

--- a/src/Pure/General/json_api.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/General/json_api.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -6,8 +6,6 @@
 
 package isabelle
 
-import java.net.URL
-
 
 object JSON_API {
   val mime_type = "application/vnd.api+json"
@@ -15,11 +13,11 @@
   def api_error(msg: String): Nothing = error("JSON API error: " + msg)
   def api_errors(msgs: List[String]): Nothing = error(("JSON API errors:" :: msgs).mkString("\n  "))
 
-  class Service(val url: URL) {
+  class Service(val url: Url) {
     override def toString: String = url.toString
 
     def get(route: String): HTTP.Content =
-      HTTP.Client.get(Url.resolve(url, route))
+      HTTP.Client.get(url.resolve(route))
 
     def get_root(route: String = ""): Root =
       Root(get(if_proper(route, "/" + route)).json)

--- a/src/Pure/General/mailman.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/General/mailman.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -7,8 +7,6 @@
 package isabelle
 
 
-import java.net.URL
-
 import scala.annotation.tailrec
 import scala.util.matching.Regex
 import scala.util.matching.Regex.Match
@@ -319,7 +317,7 @@
   /* mailing list archives */
 
   abstract class Archive(
-    url: URL,
+    url: Url,
     name: String = "",
     tag: String = ""
   ) {
@@ -340,7 +338,7 @@
     def make_body(lines: List[String]): String =
       cat_lines(Library.take_suffix[String](_.isEmpty, lines)._1)
 
-    private val main_url: URL =
+    private val main_url: Url =
       Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
 
     private val main_html = Url.read(main_url)
@@ -356,7 +354,7 @@
 
     def list_tag: String = proper_string(tag).getOrElse(list_name)
 
-    def read_text(href: String): String = Url.read(Url.resolve(main_url, href))
+    def read_text(href: String): String = Url.read(main_url.resolve(href))
 
     def hrefs_text: List[String] =
       """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(main_html).map(_.group(1)).toList
@@ -371,8 +369,8 @@
     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 = Url.resolve(main_url, href)
-      val connection = url.openConnection
+      val url = main_url.resolve(href)
+      val connection = url.open_connection()
       try {
         val length = connection.getContentLengthLong
         val timestamp = connection.getLastModified

--- a/src/Pure/General/scan.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/General/scan.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -14,7 +14,6 @@
   Reader, CharSequenceReader, PagedSeq}
 import scala.util.parsing.combinator.RegexParsers
 import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
-import java.net.URL
 
 
 object Scan {
@@ -427,8 +426,8 @@
   def byte_reader(file: JFile): Byte_Reader =
     make_byte_reader(new FileInputStream(file), file.length.toInt)
 
-  def byte_reader(url: URL): Byte_Reader = {
-    val connection = url.openConnection
+  def byte_reader(url: Url): Byte_Reader = {
+    val connection = url.open_connection()
     val stream = connection.getInputStream
     val stream_length = connection.getContentLength
     make_byte_reader(stream, stream_length)

--- a/src/Pure/General/url.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/General/url.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -1,15 +1,16 @@
 /*  Title:      Pure/General/url.scala
     Author:     Makarius
 
-Basic URL operations.
+Basic URL/URI operations.
 */
 
 package isabelle
 
 
-import java.io.{File => JFile}
+import java.io.{File => JFile, InputStream}
 import java.nio.file.{Paths, FileSystemNotFoundException}
-import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
+import java.net.{URI, URISyntaxException, MalformedURLException, URLDecoder, URLEncoder,
+  URLConnection}
 import java.util.Locale
 import java.util.zip.GZIPInputStream
 
@@ -36,30 +37,33 @@
     exn.isInstanceOf[URISyntaxException] ||
     exn.isInstanceOf[IllegalArgumentException]
 
-  def apply(name: String): URL =
-    try { new URI(name).toURL }
-    catch {
-      case exn: Throwable if is_malformed(exn) => error("Malformed URL " + quote(name))
-    }
+  def apply(uri: URI): Url = new Url(uri)
 
-  def resolve(url: URL, route: String): URL =
-    if (route.isEmpty) url else url.toURI.resolve(route).toURL
+  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 is_wellformed(name: String): Boolean =
     try { Url(name); true }
     catch { case ERROR(_) => false }
 
   def is_readable(name: String): Boolean =
-    try { Url(name).openStream.close(); true }
+    try { Url(name).open_stream().close(); true }
     catch { case ERROR(_) => false }
 
 
   /* file name */
 
-  def file_name(url: URL): String =
-    Library.take_suffix[Char](c => c != '/' && c != '\\', url.getFile.toString.toList)._2.mkString
+  def file_name(url: Url): String =
+    Library.take_suffix[Char](c => c != '/' && c != '\\',
+      url.java_url.getFile.toString.toList)._2.mkString
 
-  def trim_index(url: URL): URL = {
+  def trim_index(url: Url): Url = {
     Library.try_unprefix("/index.html", url.toString) match {
       case Some(u) => Url(u)
       case None =>
@@ -79,12 +83,12 @@
 
   /* read */
 
-  private def read(url: URL, gzip: Boolean): String =
-    using(url.openStream)(stream =>
+  private def read(url: Url, gzip: Boolean): String =
+    using(url.open_stream())(stream =>
       File.read_stream(if (gzip) new GZIPInputStream(stream) else stream))
 
-  def read(url: URL): String = read(url, false)
-  def read_gzip(url: URL): String = read(url, true)
+  def read(url: Url): String = read(url, false)
+  def read_gzip(url: Url): String = read(url, true)
 
   def read(name: String): String = read(Url(name), false)
   def read_gzip(name: String): String = read(Url(name), true)
@@ -146,3 +150,21 @@
 
   def direct_path(prefix: String): String = append_path(prefix, ".")
 }
+
+final class Url private(val uri: URI) {
+  override def toString: String = uri.toString
+
+  override def hashCode: Int = uri.hashCode
+  override def equals(obj: Any): Boolean =
+    obj match {
+      case other: Url => uri == other.uri
+      case _ => false
+    }
+
+  def resolve(route: String): Url =
+    if (route.isEmpty) this else new Url(uri.resolve(route))
+
+  def java_url: java.net.URL = uri.toURL
+  def open_stream(): InputStream = java_url.openStream()
+  def open_connection(): URLConnection = java_url.openConnection()
+}

--- a/src/Pure/Tools/flarum.scala	Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/Tools/flarum.scala	Sun Jan 21 14:05:14 2024 +0100
@@ -7,16 +7,13 @@
 package isabelle
 
 
-import java.net.URL
-
-
 object Flarum {
   // see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
   val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
 
-  def server(url: URL): Server = new Server(url)
+  def server(url: Url): Server = new Server(url)
 
-  class Server private[Flarum](url: URL) extends JSON_API.Service(url) {
+  class Server private[Flarum](url: Url) extends JSON_API.Service(url) {
     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")