# HG changeset patch # User wenzelm # Date 1699736737 -3600 # Node ID 4e1dc465dfccced2aca775b6fa162988354a78a8 # Parent c8c40e11c907387eb5dae8045e234525253d5f29 clarified modules; diff -r c8c40e11c907 -r 4e1dc465dfcc src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Nov 11 21:25:20 2023 +0100 +++ b/src/Pure/General/file.scala Sat Nov 11 22:05:37 2023 +0100 @@ -131,15 +131,6 @@ def bash_platform_path(path: Path): String = Bash.string(platform_path(path)) - /* directory entries */ - - def check_dir(path: Path): Path = - if (path.is_dir) path else error("No such directory: " + path) - - def check_file(path: Path): Path = - if (path.is_file) path else error("No such file: " + path) - - /* directory content */ def read_dir(dir: Path): List[String] = { @@ -420,5 +411,5 @@ /* space */ def space(path: Path): Space = - Space.bytes(check_file(path).file.length) + Space.bytes(path.check_file.file.length) } diff -r c8c40e11c907 -r 4e1dc465dfcc src/Pure/General/path.scala --- 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)