src/Pure/PIDE/command.scala
changeset 46164 a01c969f2e14
parent 46152 793cecd4ffc0
child 46712 8650d9a95736
equal deleted inserted replaced
46163:6c880b26dfc4 46164:a01c969f2e14
    32       message match {
    32       message match {
    33         case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
    33         case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
    34           (this /: msgs)((state, msg) =>
    34           (this /: msgs)((state, msg) =>
    35             msg match {
    35             msg match {
    36               case elem @ XML.Elem(markup, Nil) =>
    36               case elem @ XML.Elem(markup, Nil) =>
    37                 val info: Text.Markup = Text.Info(command.range, elem)
    37                 state.add_status(markup).add_markup(Text.Info(command.range, elem))
    38                 state.add_status(markup).add_markup(info)
       
    39 
    38 
    40               case _ => System.err.println("Ignored status message: " + msg); state
    39               case _ => System.err.println("Ignored status message: " + msg); state
    41             })
    40             })
    42 
    41 
    43         case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
    42         case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>