src/Pure/PIDE/isar_document.scala
changeset 39511 5f318522e6fe
parent 39441 4110cc1b8f9f
child 39622 53365ba766ac
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Sep 17 21:04:56 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 21:49:34 2010 +0200
     1.3 @@ -70,7 +70,19 @@
     1.4      }
     1.5  
     1.6  
     1.7 -  /* reported positions */
     1.8 +  /* specific messages */
     1.9 +
    1.10 +  def is_warning(msg: XML.Tree): Boolean =
    1.11 +    msg match {
    1.12 +      case XML.Elem(Markup(Markup.WARNING, _), _) => true
    1.13 +      case _ => false
    1.14 +    }
    1.15 +
    1.16 +  def is_error(msg: XML.Tree): Boolean =
    1.17 +    msg match {
    1.18 +      case XML.Elem(Markup(Markup.ERROR, _), _) => true
    1.19 +      case _ => false
    1.20 +    }
    1.21  
    1.22    def is_state(msg: XML.Tree): Boolean =
    1.23      msg match {
    1.24 @@ -78,6 +90,9 @@
    1.25        case _ => false
    1.26      }
    1.27  
    1.28 +
    1.29 +  /* reported positions */
    1.30 +
    1.31    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.32  
    1.33    def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =