# HG changeset patch
# User wenzelm
# Date 1618222609 -7200
# Node ID c83152933579ef5b6ca3c0255042e411e4fb916c
# Parent  a578ebf5b78d81a7526b13843dae04a3d7b9c1bb
clarified signature: Bytes extends CharSequence already (see d201996f72a8);

diff -r a578ebf5b78d -r c83152933579 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon Apr 12 11:45:16 2021 +0200
+++ b/src/Pure/General/bytes.scala	Mon Apr 12 12:16:49 2021 +0200
@@ -134,11 +134,7 @@
     a
   }
 
-  def text: String =
-    UTF8.decode_chars(identity, bytes, offset, offset + length).toString
-
-  def symbols: String =
-    UTF8.decode_chars(Symbol.decode, bytes, offset, offset + length).toString
+  def text: String = UTF8.decode_permissive(this)
 
   def base64: String =
   {
diff -r a578ebf5b78d -r c83152933579 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Mon Apr 12 11:45:16 2021 +0200
+++ b/src/Pure/General/utf8.scala	Mon Apr 12 12:16:49 2021 +0200
@@ -29,7 +29,8 @@
 
   def decode_permissive(text: CharSequence): String =
   {
-    val buf = new java.lang.StringBuilder(text.length)
+    val len = text.length
+    val buf = new java.lang.StringBuilder(len)
     var code = -1
     var rest = 0
     def flush(): Unit =
@@ -57,7 +58,7 @@
         rest -= 1
       }
     }
-    for (i <- 0 until text.length) {
+    for (i <- 0 until len) {
       val c = text.charAt(i)
       if (c < 128) { flush(); buf.append(c) }
       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
@@ -68,23 +69,4 @@
     flush()
     buf.toString
   }
-
-  private class Decode_Chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
-  {
-    def length: Int = end - start
-    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
-    def subSequence(i: Int, j: Int): CharSequence =
-      new Decode_Chars(decode, buffer, start + i, start + j)
-
-    // toString with adhoc decoding: abuse of CharSequence interface
-    override def toString: String = decode(decode_permissive(this))
-  }
-
-  def decode_chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int): CharSequence =
-  {
-    require(0 <= start && start <= end && end <= buffer.length, "bad decode range")
-    new Decode_Chars(decode, buffer, start, end)
-  }
 }
diff -r a578ebf5b78d -r c83152933579 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Apr 12 11:45:16 2021 +0200
+++ b/src/Pure/PIDE/prover.scala	Mon Apr 12 12:16:49 2021 +0200
@@ -263,7 +263,8 @@
 
   private def message_output(stream: InputStream): Thread =
   {
-    def decode_chunk(chunk: Bytes): XML.Body = YXML.parse_body_failsafe(chunk.symbols)
+    def decode_chunk(chunk: Bytes): XML.Body =
+      Symbol.decode_yxml_failsafe(chunk.text)
 
     val thread_name = "message_output"
     Isabelle_Thread.fork(name = thread_name) {