diff -r 953953504590 -r 84990c95712d src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jul 26 20:35:42 2022 +0200
+++ b/src/Pure/General/file.scala	Wed Jul 27 09:03:06 2022 +0200
@@ -13,7 +13,7 @@
 import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
   FileVisitOption, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
-import java.net.{URL, MalformedURLException}
+import java.net.{URI, URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.EnumSet
 
@@ -62,6 +62,12 @@
   def path(file: JFile): Path = Path.explode(standard_path(file))
   def pwd(): Path = path(Path.current.absolute_file)
 
+  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)
+
 
   /* relative paths */