diff -r 7a6cba7c77c9 -r 52154fef991d src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Tue Jun 11 16:02:33 2024 +0200 +++ b/src/Pure/General/bytes.scala Tue Jun 11 16:32:10 2024 +0200 @@ -132,7 +132,7 @@ final class Bytes private( protected val bytes: Array[Byte], protected val offset: Int, - val length: Int) extends Bytes.Vec with CharSequence { + val length: Int) extends Bytes.Vec { /* equality */ override def equals(that: Any): Boolean = { @@ -224,21 +224,18 @@ else throw new IndexOutOfBoundsException - /* CharSequence operations */ - - def charAt(i: Int): Char = apply(i).asInstanceOf[Char] + /* slice */ - def subSequence(i: Int, j: Int): Bytes = { - if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i) + def slice(i: Long, j: Long): Bytes = + if (0 <= i && i <= j && j <= size) new Bytes(bytes, (offset + i).toInt, (j - i).toInt) else throw new IndexOutOfBoundsException - } def trim_line: Bytes = - if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10) { - subSequence(0, length - 2) + if (size >= 2 && apply(size - 2) == 13 && apply(size - 1) == 10) { + slice(0, size - 2) } - else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10)) { - subSequence(0, length - 1) + else if (size >= 1 && (apply(size - 1) == 13 || apply(size - 1) == 10)) { + slice(0, size - 1) } else this