# HG changeset patch
# User wenzelm
# Date 1699737434 -3600
# Node ID db9dba720ac7d5de9da13a1c997563d71d04c688
# Parent  b6116a86d2acc7d06f428ec10fb500af14aeed26
proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);

diff -r b6116a86d2ac -r db9dba720ac7 src/Pure/General/bytes.scala
--- 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)