prefer strict operation: java.io.File.length returns 0 for non-existent file;

--- a/src/Pure/General/file.scala	Fri Jan 27 15:33:21 2023 +0100
+++ b/src/Pure/General/file.scala	Fri Jan 27 15:43:45 2023 +0100
@@ -404,5 +404,5 @@
   /* space */
 
   def space(path: Path): Space =
-    Space.bytes(path.file.length)
+    Space.bytes(check_file(path).file.length)
 }