--- a/src/Pure/General/bytes.scala Wed Jul 03 20:18:36 2024 +0200
+++ b/src/Pure/General/bytes.scala Wed Jul 03 20:35:10 2024 +0200
@@ -10,6 +10,7 @@
import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream,
InputStream, OutputStream, File => JFile}
import java.nio.ByteBuffer
+import java.nio.charset.StandardCharsets.ISO_8859_1
import java.nio.channels.FileChannel
import java.nio.file.StandardOpenOption
import java.util.Arrays
@@ -45,6 +46,10 @@
val empty: Bytes = reuse_array(new Array(0))
+ def raw(s: String): Bytes =
+ if (s.isEmpty) empty
+ else Builder.use(hint = s.length) { builder => builder += s.getBytes(ISO_8859_1) }
+
def apply(s: String): Bytes =
if (s.isEmpty) empty
else Builder.use(hint = s.length) { builder => builder += s }
@@ -131,21 +136,6 @@
def append(path: Path, bytes: Bytes): Unit = append(path.file, bytes)
- /* vector of short unsigned integers */
-
- trait Vec {
- def size: Long
- def apply(i: Long): Char
- }
-
- class Vec_String(string: String) extends Vec {
- override def size: Long = string.length.toLong
- override def apply(i: Long): Char =
- if (0 <= i && i < size) string(i.toInt)
- else throw new IndexOutOfBoundsException
- }
-
-
/* incremental builder: unsynchronized! */
object Builder {
@@ -294,7 +284,7 @@
protected val chunk0: Array[Byte],
protected val offset: Long,
val size: Long
-) extends Bytes.Vec with YXML.Source {
+) extends YXML.Source {
bytes =>
assert(
@@ -499,7 +489,7 @@
}
utf8
- if (utf8) UTF8.decode_permissive_bytes(bytes)
+ if (utf8) UTF8.decode_permissive(bytes)
else new String(make_array, UTF8.charset)
}