# HG changeset patch
# User wenzelm
# Date 1718530882 -7200
# Node ID 061d672570f56b197049b17799bb72e0a260a5d0
# Parent  224cdaaaf0cd8bfd93ab7a8463f30b462f0a400f
tuned names;

diff -r 224cdaaaf0cd -r 061d672570f5 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Jun 16 11:28:47 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sun Jun 16 11:41:22 2024 +0200
@@ -61,7 +61,7 @@
     if (limit == 0) empty
     else {
       Builder.use(hint = if (limit > 0) limit else hint) { builder =>
-        val buf = new Array[Byte](Bytes.block_size)
+        val buf = new Array[Byte](block_size)
         var m = 0
         var n = 0L
         while ({
@@ -82,13 +82,13 @@
   def read_file(path: Path, offset: Long = 0L, limit: Long = -1L): Bytes = {
     val length = File.size(path)
     val start = offset.max(0L)
-    val len = (length - start).max(0L).min(if (limit < 0) Long.MaxValue else limit)
-    if (len == 0L) empty
+    val stop = (length - start).max(0L).min(if (limit < 0) Long.MaxValue else limit)
+    if (stop == 0L) empty
     else {
-      Builder.use(hint = len) { builder =>
+      Builder.use(hint = stop) { builder =>
         using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { channel =>
           channel.position(start)
-          val buf = ByteBuffer.allocate(Bytes.block_size)
+          val buf = ByteBuffer.allocate(block_size)
           var m = 0
           var n = 0L
           while ({
@@ -98,7 +98,7 @@
               buf.clear()
               n += m
             }
-            m != -1 && len > n
+            m != -1 && stop > n
           }) ()
         }
       }