some specific message classification;
authorwenzelm
Fri, 17 Sep 2010 21:49:34 +0200
changeset 39511 5f318522e6fe
parent 39510 d9f5f01faa1b
child 39512 31290f54be19
some specific message classification;
src/Pure/PIDE/isar_document.scala
--- 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] =