58 state |
58 state |
59 }) |
59 }) |
60 case XML.Elem(Markup(name, atts), body) => |
60 case XML.Elem(Markup(name, atts), body) => |
61 atts match { |
61 atts match { |
62 case Isabelle_Markup.Serial(i) => |
62 case Isabelle_Markup.Serial(i) => |
63 val props = Position.purge(atts) |
63 val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), atts), body) |
64 val result = XML.Elem(Markup(name, props), body) |
64 val message2 = XML.Elem(Markup(name, Position.purge(atts)), body) |
65 val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body) |
|
66 |
65 |
67 val st0 = copy(results = results + (i -> result_message)) |
66 val st0 = copy(results = results + (i -> message1)) |
68 val st1 = |
67 val st1 = |
69 if (Protocol.is_tracing(result)) st0 |
68 if (Protocol.is_tracing(message)) st0 |
70 else |
69 else |
71 (st0 /: Protocol.message_positions(command, message))( |
70 (st0 /: Protocol.message_positions(command, message))( |
72 (st, range) => st.add_markup(Text.Info(range, result))) |
71 (st, range) => st.add_markup(Text.Info(range, message2))) |
73 |
72 |
74 st1 |
73 st1 |
75 case _ => System.err.println("Ignored message without serial number: " + message); this |
74 case _ => System.err.println("Ignored message without serial number: " + message); this |
76 } |
75 } |
77 } |
76 } |