src/Pure/Tools/debugger.scala
changeset 76022 6ce62e4e7dc0
parent 75446 691ed9f41729
child 76604 aaedcdfa2154
--- a/src/Pure/Tools/debugger.scala	Tue Aug 30 13:18:33 2022 +0200
+++ b/src/Pure/Tools/debugger.scala	Wed Aug 31 15:05:28 2022 +0200
@@ -124,7 +124,7 @@
         case Markup.Debugger_Output(thread_name) =>
           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)
+              val message = Protocol.make_message(body, kind = name, props = props)
               debugger.add_output(thread_name, i -> session.cache.elem(message))
               true
             case _ => false