--- 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
}