src/Pure/PIDE/command.scala
changeset 55622 ce575c2212fc
parent 55618 995162143ef4
child 55648 38f264741609
--- a/src/Pure/PIDE/command.scala	Thu Feb 20 16:08:39 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Feb 20 16:56:51 2014 +0100
@@ -90,8 +90,7 @@
           (this /: msgs)((state, msg) =>
             msg match {
               case elem @ XML.Elem(markup, Nil) =>
-                state.add_status(markup)
-                  .add_markup("", Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
+                state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
 
               case _ =>
                 System.err.println("Ignored status message: " + msg)