# HG changeset patch
# User wenzelm
# Date 1489443284 -3600
# Node ID edd3f532e4e3f1181e6329cf7fe08035e31b7051
# Parent  060a8a1f2dec8fd13bdd2cda585eb6ce797c49a0
tuned;

diff -r 060a8a1f2dec -r edd3f532e4e3 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Mar 13 22:50:26 2017 +0100
+++ b/src/Pure/Tools/debugger.scala	Mon Mar 13 23:14:44 2017 +0100
@@ -152,12 +152,10 @@
     {
       msg.properties match {
         case Markup.Debugger_Output(thread_name) =>
-          val msg_body =
-            prover.xml_cache.body(
-              YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))))
-          msg_body match {
+          YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
-              val message = XML.Elem(Markup(Markup.message(name), props), body)
+              val message =
+                prover.xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
               the_debugger.add_output(thread_name, i -> message)
               true
             case _ => false