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