src/Pure/PIDE/isar_document.scala
changeset 39181 2257eded8323
parent 39175 a08d68e993ea
child 39439 1c294d150ded
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 23:53:27 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 23:59:14 2010 +0200
     1.3 @@ -56,21 +56,6 @@
     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)