Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
authorwenzelm
Tue Sep 07 16:40:30 2010 +0200 (2010-09-07)
changeset 3917231b95e0da7b7
parent 39171 525a13b9ac74
child 39173 ed3946086358
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
src/Pure/PIDE/command.scala
src/Pure/PIDE/isar_document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Sep 07 16:08:29 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Sep 07 16:40:30 2010 +0200
     1.3 @@ -60,8 +60,8 @@
     1.4            atts match {
     1.5              case Markup.Serial(i) =>
     1.6                val result = XML.Elem(Markup(name, Position.purge(atts)), body)
     1.7 -              (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
     1.8 -                (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
     1.9 +              (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
    1.10 +                (st, range) => st.add_markup(Text.Info(range, result)))
    1.11              case _ => System.err.println("Ignored message without serial number: " + message); this
    1.12            }
    1.13        }
     2.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 16:08:29 2010 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 16:40:30 2010 +0200
     2.3 @@ -67,20 +67,21 @@
     2.4        case _ => false
     2.5      }
     2.6  
     2.7 -  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
     2.8 +  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
     2.9    {
    2.10      def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    2.11        tree match {
    2.12 -        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    2.13 -        if include_pos(name) && id == command_id =>
    2.14 -          body.foldLeft(set + range)(reported)
    2.15 +        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
    2.16 +        if include_pos(name) && id == command.id =>
    2.17 +          val range = command.decode(raw_range).restrict(command.range)
    2.18 +          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
    2.19          case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
    2.20            body.foldLeft(set)(reported)
    2.21          case _ => set
    2.22        }
    2.23      val set = reported(Set.empty, message)
    2.24      if (set.isEmpty && !is_state(message))
    2.25 -      set ++ Position.Range.unapply(message.markup.properties)
    2.26 +      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
    2.27      else set
    2.28    }
    2.29  }