tuned;
authorwenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73819 55b66a45bc94
parent 73818 c5a390b9ae00
child 73820 a021bb558feb
tuned;
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))