diff -r 5d77df3d30d1 -r a4118f530263 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Feb 18 12:32:54 2024 +0100
+++ b/src/Pure/General/file.scala	Sun Feb 18 12:33:43 2024 +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}
+import java.net.URI
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.EnumSet
 
@@ -85,8 +85,8 @@
   def uri(file: JFile): URI = file.toURI
   def uri(path: Path): URI = path.file.toURI
 
-  def url(file: JFile): URL = uri(file).toURL
-  def url(path: Path): URL = url(path.file)
+  def url(file: JFile): Url = Url(uri(file))
+  def url(path: Path): Url = url(path.file)
 
 
   /* adhoc file types */