1.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Sep 02 23:17:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 02 23:26:21 2010 +0200
     1.3 @@ -58,17 +58,23 @@
     1.4  
     1.5    /* reported positions */
     1.6  
     1.7 +  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     1.8 +  private val exclude_pos = Set(Markup.LOCATION)
     1.9 +
    1.10    def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
    1.11    {
    1.12      def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.13        tree match {
    1.14          case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    1.15 -        if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
    1.16 -          id == command_id => body.foldLeft(set + range)(reported)
    1.17 -        case XML.Elem(_, body) => body.foldLeft(set)(reported)
    1.18 -        case XML.Text(_) => set
    1.19 +        if include_pos(name) && id == command_id =>
    1.20 +          body.foldLeft(set + range)(reported)
    1.21 +        case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
    1.22 +          body.foldLeft(set)(reported)
    1.23 +        case _ => set
    1.24        }
    1.25 -    reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
    1.26 +    val set = reported(Set.empty, message)
    1.27 +    if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
    1.28 +    else set
    1.29    }
    1.30  }
    1.31