--- a/src/Pure/PIDE/isar_document.scala Tue Sep 07 17:34:28 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Tue Sep 07 18:44:28 2010 +0200
@@ -56,6 +56,21 @@
}
+ /* result messages */
+
+ def is_warning(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WARNING, _), _) => true
+ case _ => false
+ }
+
+ def is_error(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.ERROR, _), _) => true
+ case _ => false
+ }
+
+
/* reported positions */
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)