changeset 49445 | 638cefe3ee99 |
parent 49418 | c451856129cd |
child 49466 | 99ed1f422635 |
--- a/src/Pure/PIDE/command.scala Wed Sep 19 14:47:15 2012 +0200 +++ b/src/Pure/PIDE/command.scala Wed Sep 19 17:07:25 2012 +0200 @@ -70,8 +70,8 @@ else (st0 /: Protocol.message_positions(command, message))( (st, range) => st.add_markup(Text.Info(range, result))) - val st2 = (st1 /: Protocol.message_reports(message))(_ + _) - st2 + + st1 case _ => System.err.println("Ignored message without serial number: " + message); this } }