src/Pure/PIDE/protocol.scala
changeset 52650 4cf6fbf1d9a1
parent 52582 31467a4b1466
child 52760 8517172b9626
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Jul 13 17:05:22 2013 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Jul 13 18:13:09 2013 +0200
     1.3 @@ -205,15 +205,18 @@
     1.4        case _ => false
     1.5      }
     1.6  
     1.7 -  def is_state(msg: XML.Tree): Boolean =
     1.8 +  def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
     1.9      msg match {
    1.10        case XML.Elem(Markup(Markup.WRITELN, _),
    1.11 -        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.12 +        List(XML.Elem(markup, _))) => markup.name == name
    1.13        case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
    1.14 -        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.15 +        List(XML.Elem(markup, _))) => markup.name == name
    1.16        case _ => false
    1.17      }
    1.18  
    1.19 +  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
    1.20 +  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
    1.21 +
    1.22    def is_warning(msg: XML.Tree): Boolean =
    1.23      msg match {
    1.24        case XML.Elem(Markup(Markup.WARNING, _), _) => true