src/Pure/PIDE/protocol.scala
changeset 49418 c451856129cd
parent 49039 e780d1bf767e
child 49445 638cefe3ee99
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Sep 18 15:55:29 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Sep 18 17:20:40 2012 +0200
     1.3 @@ -135,18 +135,21 @@
     1.4   def is_tracing(msg: XML.Tree): Boolean =
     1.5      msg match {
     1.6        case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
     1.7 +      case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
     1.8        case _ => false
     1.9      }
    1.10  
    1.11    def is_warning(msg: XML.Tree): Boolean =
    1.12      msg match {
    1.13        case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
    1.14 +      case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
    1.15        case _ => false
    1.16      }
    1.17  
    1.18    def is_error(msg: XML.Tree): Boolean =
    1.19      msg match {
    1.20        case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
    1.21 +      case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
    1.22        case _ => false
    1.23      }
    1.24  
    1.25 @@ -154,6 +157,8 @@
    1.26      msg match {
    1.27        case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
    1.28          List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
    1.29 +      case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
    1.30 +        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
    1.31        case _ => false
    1.32      }
    1.33