src/Pure/PIDE/protocol.scala
changeset 59184 830bb7ddb3ab
parent 59085 08a6901eb035
child 59203 5f0bd5afc16d
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Dec 23 16:00:38 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Dec 23 20:46:42 2014 +0100
     1.3 @@ -227,12 +227,17 @@
     1.4        case _ => false
     1.5      }
     1.6  
     1.7 -  def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
     1.8 +  def is_state(msg: XML.Tree): Boolean =
     1.9      msg match {
    1.10 -      case XML.Elem(Markup(Markup.WRITELN, _),
    1.11 -        List(XML.Elem(markup, _))) => markup.name == name
    1.12 -      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
    1.13 -        List(XML.Elem(markup, _))) => markup.name == name
    1.14 +      case XML.Elem(Markup(Markup.STATE, _), _) => true
    1.15 +      case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
    1.16 +      case _ => false
    1.17 +    }
    1.18 +
    1.19 +  def is_information(msg: XML.Tree): Boolean =
    1.20 +    msg match {
    1.21 +      case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
    1.22 +      case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
    1.23        case _ => false
    1.24      }
    1.25  
    1.26 @@ -259,8 +264,6 @@
    1.27        case _ => false
    1.28      }
    1.29  
    1.30 -  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
    1.31 -  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
    1.32    def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
    1.33  
    1.34    def is_inlined(msg: XML.Tree): Boolean =