src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/General/path.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -10,6 +10,7 @@
 
 import java.util.{Map => JMap}
 import java.io.{File => JFile}
+import java.nio.file.{Path => JPath}
 
 import scala.util.matching.Regex
 
@@ -306,6 +307,8 @@
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 
+  def java_path: JPath = file.toPath
+
   def absolute_file: JFile = File.absolute(file)
   def canonical_file: JFile = File.canonical(file)