src/Pure/PIDE/isar_document.scala
changeset 39622 53365ba766ac
parent 39511 5f318522e6fe
child 39625 fb0c851e4f9d
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:25:21 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:39:17 2010 +0200
     1.3 @@ -72,6 +72,12 @@
     1.4  
     1.5    /* specific messages */
     1.6  
     1.7 +  def is_tracing(msg: XML.Tree): Boolean =
     1.8 +    msg match {
     1.9 +      case XML.Elem(Markup(Markup.TRACING, _), _) => true
    1.10 +      case _ => false
    1.11 +    }
    1.12 +
    1.13    def is_warning(msg: XML.Tree): Boolean =
    1.14      msg match {
    1.15        case XML.Elem(Markup(Markup.WARNING, _), _) => true