# HG changeset patch
# User wenzelm
# Date 1708256023 -3600
# Node ID a4118f5302639b8bacd30ea150e8ee30ff8572b9
# Parent  5d77df3d30d190893161ef4c9e67eb9e8b13a5cf
clarified signature: avoid ill-defined type java.net.URL;

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 */
diff -r 5d77df3d30d1 -r a4118f530263 src/Pure/System/classpath.scala
--- a/src/Pure/System/classpath.scala	Sun Feb 18 12:32:54 2024 +0100
+++ b/src/Pure/System/classpath.scala	Sun Feb 18 12:33:43 2024 +0100
@@ -55,7 +55,8 @@
     val this_class_loader = this.getClass.getClassLoader
     if (dynamic_jars.isEmpty) this_class_loader
     else {
-      new URLClassLoader(dynamic_jars.map(File.url).toArray, this_class_loader) {
+      val dynamic_jars_url = dynamic_jars.map(file => File.url(file).java_url)
+      new URLClassLoader(dynamic_jars_url.toArray, this_class_loader) {
         override def finalize(): Unit = {
           for (jar <- dynamic_jars) {
             try { jar.delete() }