tuned;
authorwenzelm
Mon, 13 Mar 2017 23:14:44 +0100
changeset 65217 edd3f532e4e3
parent 65216 060a8a1f2dec
child 65218 102b8e092860
tuned;
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