--- a/src/Pure/General/path.scala Sat Nov 11 21:25:20 2023 +0100
+++ b/src/Pure/General/path.scala Sat Nov 11 22:05:37 2023 +0100
@@ -323,9 +323,13 @@
/* platform files */
def file: JFile = File.platform_file(this)
+
def is_file: Boolean = file.isFile
def is_dir: Boolean = file.isDirectory
+ def check_file: Path = if (is_file) this else error("No such file: " + this)
+ def check_dir: Path = if (is_dir) this else error("No such directory: " + this)
+
def java_path: JPath = file.toPath
def absolute_file: JFile = File.absolute(file)