src/Pure/PIDE/isar_document.scala
changeset 39172 31b95e0da7b7
parent 39170 04ad0fed81f5
child 39175 a08d68e993ea
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 16:08:29 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 16:40:30 2010 +0200
     1.3 @@ -67,20 +67,21 @@
     1.4        case _ => false
     1.5      }
     1.6  
     1.7 -  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
     1.8 +  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
     1.9    {
    1.10      def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.11        tree match {
    1.12 -        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    1.13 -        if include_pos(name) && id == command_id =>
    1.14 -          body.foldLeft(set + range)(reported)
    1.15 +        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
    1.16 +        if include_pos(name) && id == command.id =>
    1.17 +          val range = command.decode(raw_range).restrict(command.range)
    1.18 +          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
    1.19          case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
    1.20            body.foldLeft(set)(reported)
    1.21          case _ => set
    1.22        }
    1.23      val set = reported(Set.empty, message)
    1.24      if (set.isEmpty && !is_state(message))
    1.25 -      set ++ Position.Range.unapply(message.markup.properties)
    1.26 +      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
    1.27      else set
    1.28    }
    1.29  }