# 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)