tuned names;
authorwenzelm
Sun, 16 Jun 2024 11:41:22 +0200
changeset 80384 061d672570f5
parent 80383 224cdaaaf0cd
child 80385 605e19319343
tuned names;
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
           }) ()
         }
       }