src/Pure/PIDE/isar_document.scala
changeset 39439 1c294d150ded
parent 39181 2257eded8323
child 39441 4110cc1b8f9f
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Sep 16 15:37:12 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 15:51:11 2010 +0200
     1.3 @@ -56,10 +56,16 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* messages */
     1.8 +
     1.9 +  def clean_message(body: XML.Body): XML.Body =
    1.10 +    body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
    1.11 +      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    1.12 +
    1.13 +
    1.14    /* reported positions */
    1.15  
    1.16    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.17 -  private val exclude_pos = Set(Markup.LOCATION)
    1.18  
    1.19    private def is_state(msg: XML.Tree): Boolean =
    1.20      msg match {
    1.21 @@ -75,8 +81,7 @@
    1.22          if include_pos(name) && id == command.id =>
    1.23            val range = command.decode(raw_range).restrict(command.range)
    1.24            body.foldLeft(if (range.is_singularity) set else set + range)(reported)
    1.25 -        case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
    1.26 -          body.foldLeft(set)(reported)
    1.27 +        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(reported)
    1.28          case _ => set
    1.29        }
    1.30      val set = reported(Set.empty, message)