src/Pure/PIDE/protocol.scala
changeset 67923 3e072441c96a
parent 67915 d827728b74b3
child 68321 daca5f2a0c90
     1.1 --- a/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:20:53 2018 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:39:22 2018 +0100
     1.3 @@ -239,6 +239,13 @@
     1.4        case _ => false
     1.5      }
     1.6  
     1.7 +  def is_writeln(msg: XML.Tree): Boolean =
     1.8 +    msg match {
     1.9 +      case XML.Elem(Markup(Markup.WRITELN, _), _) => true
    1.10 +      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
    1.11 +      case _ => false
    1.12 +    }
    1.13 +
    1.14    def is_warning(msg: XML.Tree): Boolean =
    1.15      msg match {
    1.16        case XML.Elem(Markup(Markup.WARNING, _), _) => true
    1.17 @@ -263,6 +270,9 @@
    1.18    def is_inlined(msg: XML.Tree): Boolean =
    1.19      !(is_result(msg) || is_tracing(msg) || is_state(msg))
    1.20  
    1.21 +  def is_exported(msg: XML.Tree): Boolean =
    1.22 +    is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
    1.23 +
    1.24  
    1.25    /* breakpoints */
    1.26