# HG changeset patch
# User wenzelm
# Date 1718540391 -7200
# Node ID 52f71e3816d8848d5d3bb0fd6a43d2e6b56d899e
# Parent  afaac8c6048e159dc738af84d0dd80fc2849480f
more scalable stream read operations;

diff -r afaac8c6048e -r 52f71e3816d8 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Jun 16 11:59:16 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sun Jun 16 14:19:51 2024 +0200
@@ -467,7 +467,26 @@
           else -1
         }
 
-        override def readAllBytes(): Array[Byte] = make_array
+        override def read(buffer: Array[Byte], start: Int, length: Int): Int = {
+          if (length < 16) super.read(buffer, start, length)
+          else {
+            val index0 = index
+            index = (index + length) min size
+            val n = (index - index0).toInt
+            if (n == 0) -1
+            else {
+              var i = start
+              for (a <- slice(index0, index).subarray_iterator) {
+                val l = a.length
+                if (l > 0) {
+                  System.arraycopy(a.array, a.offset, buffer, i, l)
+                  i += l
+                }
+              }
+              n
+            }
+          }
+        }
       }
     }