diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala
+++ b/src/Pure/General/bytes.scala
@@ -1,218 +1,214 @@
 /*  Title:      Pure/General/bytes.scala
     Author:     Makarius
 
 Immutable byte vectors versus UTF8 strings.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
   OutputStream, InputStream, FileInputStream, FileOutputStream}
 import java.net.URL
 import java.util.Base64
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
 
 object Bytes
 {
   val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
 
   def apply(s: CharSequence): Bytes =
   {
     val str = s.toString
     if (str.isEmpty) empty
     else {
       val b = UTF8.bytes(str)
       new Bytes(b, 0, b.length)
     }
   }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
 
   def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
     if (length == 0) empty
     else {
       val b = new Array[Byte](length)
       System.arraycopy(a, offset, b, 0, length)
       new Bytes(b, 0, b.length)
     }
 
   val newline: Bytes = apply("\n")
 
   def base64(s: String): Bytes =
   {
     val a = Base64.getDecoder.decode(s)
     new Bytes(a, 0, a.length)
   }
 
 
   /* read */
 
   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
     if (limit == 0) empty
     else {
       val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
       val out = new ByteArrayOutputStream(out_size)
       val buf = new Array[Byte](8192)
       var m = 0
 
       do {
         m = stream.read(buf, 0, buf.length min (limit - out.size))
         if (m != -1) out.write(buf, 0, m)
       } while (m != -1 && limit > out.size)
 
       new Bytes(out.toByteArray, 0, out.size)
     }
 
   def read(file: JFile): Bytes =
   {
     val length = file.length
     val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
     using(new FileInputStream(file))(read_stream(_, limit = limit))
   }
 
   def read(path: Path): Bytes = read(path.file)
 
   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
 
 
   /* write */
 
   def write(file: JFile, bytes: Bytes): Unit =
     using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }
 
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
   val length: Int) extends CharSequence
 {
   /* equality */
 
   override def equals(that: Any): Boolean =
   {
     that match {
       case other: Bytes =>
         if (this eq other) true
         else if (length != other.length) false
         else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
       case _ => false
     }
   }
 
   private lazy val hash: Int =
   {
     var h = 0
     for (i <- offset until offset + length) {
       val b = bytes(i).asInstanceOf[Int] & 0xFF
       h = 31 * h + b
     }
     h
   }
 
   override def hashCode(): Int = hash
 
 
   /* content */
 
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   def is_empty: Boolean = length == 0
 
   def iterator: Iterator[Byte] =
     for (i <- (offset until (offset + length)).iterator)
       yield bytes(i)
 
   def array: Array[Byte] =
   {
     val a = new Array[Byte](length)
     System.arraycopy(bytes, offset, a, 0, length)
     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 =
   {
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
     Base64.getEncoder.encodeToString(b)
   }
 
   def maybe_base64: (Boolean, String) =
   {
     val s = text
     if (this == Bytes(s)) (false, s) else (true, base64)
   }
 
   override def toString: String = "Bytes(" + length + ")"
 
   def proper: Option[Bytes] = if (is_empty) None else Some(this)
   def proper_text: Option[String] = if (is_empty) None else Some(text)
 
   def +(other: Bytes): Bytes =
     if (other.is_empty) this
     else if (is_empty) other
     else {
       val new_bytes = new Array[Byte](length + other.length)
       System.arraycopy(bytes, offset, new_bytes, 0, length)
       System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
       new Bytes(new_bytes, 0, new_bytes.length)
     }
 
 
   /* CharSequence operations */
 
   def charAt(i: Int): Char =
     if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
     else throw new IndexOutOfBoundsException
 
   def subSequence(i: Int, j: Int): Bytes =
   {
     if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
     else throw new IndexOutOfBoundsException
   }
 
   def trim_line: Bytes =
     if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
       subSequence(0, length - 2)
     else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
       subSequence(0, length - 1)
     else this
 
 
   /* streams */
 
   def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
 
   def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
 
 
   /* XZ data compression */
 
   def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
     using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
 
   def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes =
   {
     val result = new ByteArrayOutputStream(length)
     using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
   }
 
   def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache())
     : (Boolean, Bytes) =
   {
     val compressed = compress(options = options, cache = cache)
     if (compressed.length < length) (true, compressed) else (false, this)
   }
 }
diff --git a/src/Pure/General/utf8.scala b/src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala
+++ b/src/Pure/General/utf8.scala
@@ -1,90 +1,72 @@
 /*  Title:      Pure/General/utf8.scala
     Author:     Makarius
 
 Variations on UTF-8.
 */
 
 package isabelle
 
 
 import java.nio.charset.Charset
 import scala.io.Codec
 
 
 object UTF8
 {
   /* charset */
 
   val charset_name: String = "UTF-8"
   val charset: Charset = Charset.forName(charset_name)
   def codec(): Codec = Codec(charset)
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
 
   /* permissive UTF-8 decoding */
 
   // see also https://en.wikipedia.org/wiki/UTF-8#Description
   // overlong encodings enable byte-stuffing of low-ASCII
 
   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 =
     {
       if (code != -1) {
         if (rest == 0 && Character.isValidCodePoint(code))
           buf.appendCodePoint(code)
         else buf.append('\uFFFD')
         code = -1
         rest = 0
       }
     }
     def init(x: Int, n: Int): Unit =
     {
       flush()
       code = x
       rest = n
     }
     def push(x: Int): Unit =
     {
       if (rest <= 0) init(x, -1)
       else {
         code <<= 6
         code += x
         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)
       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
       else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
       else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
     }
     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 --git a/src/Pure/PIDE/prover.scala b/src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala
+++ b/src/Pure/PIDE/prover.scala
@@ -1,326 +1,327 @@
 /*  Title:      Pure/PIDE/prover.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Prover process wrapping.
 */
 
 package isabelle
 
 
 import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
 
 
 object Prover
 {
   /* messages */
 
   sealed abstract class Message
   type Receiver = Message => Unit
 
   class Input(val name: String, val args: List[String]) extends Message
   {
     override def toString: String =
       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
         args.flatMap(s =>
           List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString
   }
 
   class Output(val message: XML.Elem) extends Message
   {
     def kind: String = message.markup.name
     def properties: Properties.T = message.markup.properties
     def body: XML.Body = message.body
 
     def is_init: Boolean = kind == Markup.INIT
     def is_exit: Boolean = kind == Markup.EXIT
     def is_stdout: Boolean = kind == Markup.STDOUT
     def is_stderr: Boolean = kind == Markup.STDERR
     def is_system: Boolean = kind == Markup.SYSTEM
     def is_status: Boolean = kind == Markup.STATUS
     def is_report: Boolean = kind == Markup.REPORT
     def is_syslog: Boolean = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body, metric = Symbol.Metric)
       if (properties.isEmpty)
         kind + " [[" + res + "]]"
       else
         kind + " " +
           (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     }
   }
 
   class Malformed(msg: String) extends Exn.User_Error("Malformed prover message: " + msg)
   def bad_header(print: String): Nothing = throw new Malformed("bad message header\n" + print)
   def bad_chunks(): Nothing = throw new Malformed("bad message chunks")
 
   def the_chunk(chunks: List[Bytes], print: => String): Bytes =
     chunks match {
       case List(chunk) => chunk
       case _ => throw new Malformed("single chunk expected: " + print)
     }
 
   class Protocol_Output(props: Properties.T, val chunks: List[Bytes])
     extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
   {
     def chunk: Bytes = the_chunk(chunks, toString)
     lazy val text: String = chunk.text
   }
 }
 
 
 class Prover(
   receiver: Prover.Receiver,
   cache: XML.Cache,
   channel: System_Channel,
   process: Bash.Process) extends Protocol
 {
   /** receiver output **/
 
   private def system_output(text: String): Unit =
   {
     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit =
   {
     receiver(new Prover.Protocol_Output(cache.props(props), chunks))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body): Unit =
   {
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
     val reports = Protocol_Message.reports(props, body)
     for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg)))
   }
 
   private def exit_message(result: Process_Result): Unit =
   {
     output(Markup.EXIT, Markup.Process_Result(result),
       List(XML.Text(result.print_return_code)))
   }
 
 
 
   /** process manager **/
 
   private val process_result: Future[Process_Result] =
     Future.thread("process_result") {
       val rc = process.join
       val timing = process.get_timing
       Process_Result(rc, timing = timing)
     }
 
   private def terminate_process(): Unit =
   {
     try { process.terminate() }
     catch {
       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
     }
   }
 
   private val process_manager = Isabelle_Thread.fork(name = "process_manager")
   {
     val stdout = physical_output(false)
 
     val (startup_failed, startup_errors) =
     {
       var finished: Option[Boolean] = None
       val result = new StringBuilder(100)
       while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
         while (finished.isEmpty && process.stderr.ready) {
           try {
             val c = process.stderr.read
             if (c == 2) finished = Some(true)
             else result += c.toChar
           }
           catch { case _: IOException => finished = Some(false) }
         }
         Time.seconds(0.05).sleep
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
     if (startup_errors != "") system_output(startup_errors)
 
     if (startup_failed) {
       terminate_process()
       process_result.join
       stdout.join
       exit_message(Process_Result(127))
     }
     else {
       val (command_stream, message_stream) = channel.rendezvous()
 
       command_input_init(command_stream)
       val stderr = physical_output(true)
       val message = message_output(message_stream)
 
       val result = process_result.join
       system_output("process terminated")
       command_input_close()
       for (thread <- List(stdout, stderr, message)) thread.join
       system_output("process_manager terminated")
       exit_message(result)
     }
     channel.shutdown()
   }
 
 
   /* management methods */
 
   def join(): Unit = process_manager.join()
 
   def terminate(): Unit =
   {
     system_output("Terminating prover process")
     command_input_close()
 
     var count = 10
     while (!process_result.is_finished && count > 0) {
       Time.seconds(0.1).sleep
       count -= 1
     }
     if (!process_result.is_finished) terminate_process()
   }
 
 
 
   /** process streams **/
 
   /* command input */
 
   private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
 
   private def command_input_close(): Unit = command_input.foreach(_.shutdown())
 
   private def command_input_init(raw_stream: OutputStream): Unit =
   {
     val name = "command_input"
     val stream = new BufferedOutputStream(raw_stream)
     command_input =
       Some(
         Consumer_Thread.fork(name)(
           consume =
             {
               case chunks =>
                 try {
                   Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
                   chunks.foreach(_.write_stream(stream))
                   stream.flush
                   true
                 }
                 catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
             },
           finish = { case () => stream.close(); system_output(name + " terminated") }
         )
       )
   }
 
 
   /* physical output */
 
   private def physical_output(err: Boolean): Thread =
   {
     val (name, reader, markup) =
       if (err) ("standard_error", process.stderr, Markup.STDERR)
       else ("standard_output", process.stdout, Markup.STDOUT)
 
     Isabelle_Thread.fork(name = name) {
       try {
         var result = new StringBuilder(100)
         var finished = false
         while (!finished) {
           //{{{
           var c = -1
           var done = false
           while (!done && (result.isEmpty || reader.ready)) {
             c = reader.read
             if (c >= 0) result.append(c.asInstanceOf[Char])
             else done = true
           }
           if (result.nonEmpty) {
             output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
             result.clear()
           }
           else {
             reader.close()
             finished = true
           }
           //}}}
         }
       }
       catch { case e: IOException => system_output(name + ": " + e.getMessage) }
       system_output(name + " terminated")
     }
   }
 
 
   /* message output */
 
   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) {
       try {
         var finished = false
         while (!finished) {
           Byte_Message.read_message(stream) match {
             case None => finished = true
             case Some(header :: chunks) =>
               decode_chunk(header) match {
                 case List(XML.Elem(Markup(name, props), Nil)) =>
                   val kind = name.intern
                   if (kind == Markup.PROTOCOL) protocol_output(props, chunks)
                   else {
                     val body = decode_chunk(Prover.the_chunk(chunks, name))
                     output(kind, props, body)
                   }
                 case _ => Prover.bad_header(header.toString)
               }
             case Some(_) => Prover.bad_chunks()
           }
         }
       }
       catch {
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
         case e: Prover.Malformed => system_output(e.getMessage)
       }
       stream.close()
 
       system_output(thread_name + " terminated")
     }
   }
 
 
 
   /** protocol commands **/
 
   var trace: Boolean = false
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit =
     command_input match {
       case Some(thread) if thread.is_active =>
         if (trace) {
           val payload = args.foldLeft(0) { case (n, b) => n + b.length }
           Output.writeln(
             "protocol_command " + name + ", args = " + args.length + ", payload = " + payload)
         }
         thread.send(Bytes(name) :: args)
       case _ => error("Inactive prover input thread for command " + quote(name))
     }
 
   def protocol_command_args(name: String, args: List[String]): Unit =
   {
     receiver(new Prover.Input(name, args))
     protocol_command_raw(name, args.map(Bytes(_)))
   }
 
   def protocol_command(name: String, args: String*): Unit =
     protocol_command_args(name, args.toList)
 }