src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/Pure/General/file.scala	Sun Nov 12 12:26:08 2023 +0100
@@ -408,8 +408,8 @@
   }
 
 
-  /* space */
+  /* strict file size */
 
-  def space(path: Path): Space =
-    Space.bytes(path.check_file.file.length)
+  def size(path: Path): Long = path.check_file.file.length
+  def space(path: Path): Space = Space.bytes(size(path))
 }