diff -r 3cee9d20308e -r e61add9d5b5e 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)