src/Pure/PIDE/protocol.scala
changeset 56495 0b9334adcf05
parent 56474 4df2727a0b5f
child 56616 abc2da18d08d
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 09 13:32:34 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 09 15:03:07 2014 +0200
     1.3 @@ -214,9 +214,6 @@
     1.4  
     1.5    /* specific messages */
     1.6  
     1.7 -  def is_inlined(msg: XML.Tree): Boolean =
     1.8 -    !(is_result(msg) || is_tracing(msg) || is_state(msg))
     1.9 -
    1.10    def is_result(msg: XML.Tree): Boolean =
    1.11      msg match {
    1.12        case XML.Elem(Markup(Markup.RESULT, _), _) => true
    1.13 @@ -239,8 +236,14 @@
    1.14        case _ => false
    1.15      }
    1.16  
    1.17 -  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
    1.18 -  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
    1.19 +  def is_warning_markup(msg: XML.Tree, name: String): Boolean =
    1.20 +    msg match {
    1.21 +      case XML.Elem(Markup(Markup.WARNING, _),
    1.22 +        List(XML.Elem(markup, _))) => markup.name == name
    1.23 +      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
    1.24 +        List(XML.Elem(markup, _))) => markup.name == name
    1.25 +      case _ => false
    1.26 +    }
    1.27  
    1.28    def is_warning(msg: XML.Tree): Boolean =
    1.29      msg match {
    1.30 @@ -256,6 +259,13 @@
    1.31        case _ => false
    1.32      }
    1.33  
    1.34 +  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
    1.35 +  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
    1.36 +  def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
    1.37 +
    1.38 +  def is_inlined(msg: XML.Tree): Boolean =
    1.39 +    !(is_result(msg) || is_tracing(msg) || is_state(msg))
    1.40 +
    1.41  
    1.42    /* dialogs */
    1.43