src/Pure/PIDE/protocol.scala
changeset 49418 c451856129cd
parent 49039 e780d1bf767e
child 49445 638cefe3ee99
--- a/src/Pure/PIDE/protocol.scala	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Sep 18 17:20:40 2012 +0200
@@ -135,18 +135,21 @@
  def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_error(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
       case _ => false
     }
 
@@ -154,6 +157,8 @@
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
         List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
+      case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
+        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
       case _ => false
     }