diff -r 14e22b525b13 -r c79df6dc2803 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Mon Jul 25 11:19:08 2022 +0200 +++ b/src/Pure/General/path.scala Mon Jul 25 14:40:45 2022 +0200 @@ -11,6 +11,7 @@ import java.util.{Map => JMap} import java.io.{File => JFile} import java.nio.file.{Path => JPath} +import java.net.{URI, URL} import scala.util.matching.Regex @@ -313,6 +314,9 @@ def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory + def uri: URI = file.toURI + def url: URL = uri.toURL + def java_path: JPath = file.toPath def absolute_file: JFile = File.absolute(file)