diff -r 6e74f0fc8a52 -r dc220d47b85e src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sat Jun 15 20:30:31 2024 +0200 +++ b/src/Pure/General/bytes.scala Sat Jun 15 20:44:09 2024 +0200 @@ -41,11 +41,9 @@ val empty: Bytes = reuse_array(new Array(0)) - def apply(s: CharSequence): Bytes = { - val str = s.toString - if (str.isEmpty) empty - else Builder.use(hint = str.length) { builder => builder += str } - } + def apply(s: CharSequence): Bytes = + if (s.isEmpty) empty + else Builder.use(hint = s.length) { builder => builder += s } def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length) @@ -168,18 +166,20 @@ buffer = new ByteArrayOutputStream } - def += (string: String): Unit = - if (string.nonEmpty) { - if (UTF8.relevant(string)) { this += UTF8.bytes(string) } + def += (s: CharSequence): Unit = { + val n = s.length + if (n > 0) { + if (UTF8.relevant(s)) { this += UTF8.bytes(s.toString) } else { synchronized { - for (c <- string) { - buffer.write(c.toByte) + for (i <- 0 until n) { + buffer.write(s.charAt(i).toByte) buffer_check() } } } } + } def += (array: Array[Byte], offset: Int, length: Int): Unit = { if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) {