proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);

--- a/src/Pure/General/bytes.scala	Sat Nov 11 22:14:38 2023 +0100
+++ b/src/Pure/General/bytes.scala	Sat Nov 11 22:17:14 2023 +0100
@@ -73,7 +73,7 @@
   def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
 
   def read_file(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
-    val length = path.file.length
+    val length = File.space(path).bytes
     val start = offset.max(0L)
     val len = (length - start).max(0L).min(limit)
     if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)