src/Pure/PIDE/command.scala
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
           }
       }