misc tuning: more uniform read_stream vs. read_file;

--- a/src/Pure/General/bytes.scala	Tue Jul 02 16:15:50 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jul 02 16:36:49 2024 +0200
@@ -63,13 +63,14 @@
     if (limit == 0) empty
     else {
       Builder.use(hint = if (limit > 0) limit else hint) { builder =>
+        val buf_size = block_size
         val buf = new Array[Byte](block_size)
         var m = 0
         var n = 0L
         while ({
-          val l = if (limit > 0) ((limit - n) min buf.length).toInt else buf.length
+          val l = if (limit > 0) (limit - n).min(buf_size).toInt else buf_size
           m = stream.read(buf, 0, l)
-          if (m != -1) {
+          if (m > 0) {
             builder += (buf, 0, m)
             n += m
           }
@@ -84,26 +85,26 @@
   def read_file(path: Path, offset: Long = 0L, limit: Long = -1L): Bytes = {
     val length = File.size(path)
     val start = offset.max(0L)
-    val stop = (length - start).max(0L).min(if (limit < 0) Long.MaxValue else limit)
-    if (stop == 0L) empty
+    val len = (length - start).max(0L).min(if (limit < 0) Long.MaxValue else limit)
+    if (len == 0L) empty
     else {
-      Builder.use(hint = stop) { builder =>
+      Builder.use(hint = len) { builder =>
         using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { channel =>
           channel.position(start)
           val buf_size = block_size
-          val buf = ByteBuffer.allocate(block_size)
+          val buf = ByteBuffer.allocate(buf_size)
           var m = 0
           var n = 0L
           while ({
-            val l = stop - n
-            if (l < buf_size) buf.limit(l.toInt)
+            val l = (len - n).min(buf_size).toInt
+            buf.limit(l)
             m = channel.read(buf)
-            if (m != -1) {
+            if (m > 0) {
               builder += (buf.array(), 0, m)
               buf.clear()
               n += m
             }
-            m != -1 && stop > n
+            m != -1 && len > n
           }) ()
         }
       }