minor performance tuning;
authorwenzelm
Sat, 15 Jun 2024 17:16:14 +0200
changeset 80367 a6c1526600b3
parent 80366 ac4d53bc8f6b
child 80368 9db395953106
minor performance tuning;
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
       }
     }