# HG changeset patch
# User wenzelm
# Date 1618229687 -7200
# Node ID 55b66a45bc9472a4432b629bbab9abc8cde7166d
# Parent  c5a390b9ae00e011156116ea8a9d97b02ac907a2
tuned;

diff -r c5a390b9ae00 -r 55b66a45bc94 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Apr 12 12:32:09 2021 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Apr 12 14:14:47 2021 +0200
@@ -112,7 +112,7 @@
     {
       msg.properties match {
         case Markup.Debugger_State(thread_name) =>
-          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.chunk))
+          val msg_body = Symbol.decode_yxml_failsafe(msg.text)
           val debug_states =
           {
             import XML.Decode._
@@ -130,7 +130,7 @@
     {
       msg.properties match {
         case Markup.Debugger_Output(thread_name) =>
-          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.chunk)) match {
+          Symbol.decode_yxml_failsafe(msg.text) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
               debugger.add_output(thread_name, i -> session.cache.elem(message))