author | wenzelm |
Mon, 09 Jan 2012 23:08:33 +0100 | |
changeset 46164 | a01c969f2e14 |
parent 46163 | 6c880b26dfc4 |
child 46165 | 0e131ca93a49 |
--- a/src/Pure/PIDE/command.scala Mon Jan 09 18:33:55 2012 +0100 +++ b/src/Pure/PIDE/command.scala Mon Jan 09 23:08:33 2012 +0100 @@ -34,8 +34,7 @@ (this /: msgs)((state, msg) => msg match { case elem @ XML.Elem(markup, Nil) => - val info: Text.Markup = Text.Info(command.range, elem) - state.add_status(markup).add_markup(info) + state.add_status(markup).add_markup(Text.Info(command.range, elem)) case _ => System.err.println("Ignored status message: " + msg); state })