src/Pure/PIDE/isar_document.scala
changeset 39175 a08d68e993ea
parent 39172 31b95e0da7b7
child 39181 2257eded8323
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 17:34:28 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 18:44:28 2010 +0200
     1.3 @@ -56,6 +56,21 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* result messages */
     1.8 +
     1.9 +  def is_warning(msg: XML.Tree): Boolean =
    1.10 +    msg match {
    1.11 +      case XML.Elem(Markup(Markup.WARNING, _), _) => true
    1.12 +      case _ => false
    1.13 +    }
    1.14 +
    1.15 +  def is_error(msg: XML.Tree): Boolean =
    1.16 +    msg match {
    1.17 +      case XML.Elem(Markup(Markup.ERROR, _), _) => true
    1.18 +      case _ => false
    1.19 +    }
    1.20 +
    1.21 +
    1.22    /* reported positions */
    1.23  
    1.24    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)