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)