src/Pure/PIDE/command.scala
changeset 50499 f496b2b7bafb
parent 50201 c26369c9eda6
child 50500 c94bba7906d2
equal deleted inserted replaced
50498:6647ba2775c1 50499:f496b2b7bafb
    36       message match {
    36       message match {
    37         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    37         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    38           (this /: msgs)((state, msg) =>
    38           (this /: msgs)((state, msg) =>
    39             msg match {
    39             msg match {
    40               case elem @ XML.Elem(markup, Nil) =>
    40               case elem @ XML.Elem(markup, Nil) =>
    41                 state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
    41                 state.add_status(markup)
       
    42                   .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
    42 
    43 
    43               case _ => System.err.println("Ignored status message: " + msg); state
    44               case _ => System.err.println("Ignored status message: " + msg); state
    44             })
    45             })
    45 
    46 
    46         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    47         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>