clarified signature: avoid ill-defined type java.net.URL;
authorwenzelm
Sun, 18 Feb 2024 12:33:43 +0100
changeset 79659 a4118f530263
parent 79658 5d77df3d30d1
child 79660 49475f8bb4cc
clarified signature: avoid ill-defined type java.net.URL;
src/Pure/General/file.scala
src/Pure/System/classpath.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 */
--- 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() }