--- a/src/Pure/PIDE/isar_document.scala Fri Sep 17 21:04:56 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Fri Sep 17 21:49:34 2010 +0200
@@ -70,7 +70,19 @@
}
- /* reported positions */
+ /* specific 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
+ }
def is_state(msg: XML.Tree): Boolean =
msg match {
@@ -78,6 +90,9 @@
case _ => false
}
+
+ /* reported positions */
+
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =