# HG changeset patch
# User wenzelm
# Date 1284752974 -7200
# Node ID 5f318522e6fe0131b55617cfd2f5bd3e15c8e498
# Parent  d9f5f01faa1b6ef7b70aa3d0468e0c2f3fa75a30
some specific message classification;

diff -r d9f5f01faa1b -r 5f318522e6fe 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] =