# HG changeset patch
# User wenzelm
# Date 1718464574 -7200
# Node ID a6c1526600b313ed9614d35dc0c92324e241e13f
# Parent  ac4d53bc8f6b9985eb58258d72ad644f683c31dc
minor performance tuning;

diff -r ac4d53bc8f6b -r a6c1526600b3 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jun 15 17:12:49 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 17:16:14 2024 +0200
@@ -412,8 +412,17 @@
     if (chunks.isEmpty) new ByteArrayInputStream(chunk0, offset.toInt, size.toInt)
     else {
       new InputStream {
-        private val it = byte_iterator
-        def read(): Int = if (it.hasNext) it.next().toInt & 0xff else -1
+        private var index = 0L
+
+        def read(): Int = {
+          if (index < size) {
+            val res = byte_unchecked(index).toInt & 0xff
+            index += 1
+            res
+          }
+          else -1
+        }
+
         override def readAllBytes(): Array[Byte] = array
       }
     }