--- 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() }