diff -r c5a8592fb5d3 -r c451856129cd src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Pure/PIDE/command.scala Tue Sep 18 17:20:40 2012 +0200 @@ -60,10 +60,13 @@ case XML.Elem(Markup(name, atts), body) => atts match { case Isabelle_Markup.Serial(i) => - val result = XML.Elem(Markup(name, Position.purge(atts)), body) - val st0 = copy(results = results + (i -> result)) + val props = Position.purge(atts) + val result = XML.Elem(Markup(name, props), body) + val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body) + + val st0 = copy(results = results + (i -> result_message)) val st1 = - if (Protocol.is_tracing(message)) st0 + if (Protocol.is_tracing(result)) st0 else (st0 /: Protocol.message_positions(command, message))( (st, range) => st.add_markup(Text.Info(range, result)))