src/Pure/PIDE/protocol.scala
changeset 46207 e76b77356ed6
parent 46166 4beb2f41ed93
child 46209 aad604f74be0
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Jan 14 13:22:39 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Jan 14 14:34:42 2012 +0100
     1.3 @@ -148,6 +148,7 @@
     1.4        tree match {
     1.5          case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
     1.6          if include_pos(name) && id == command.id =>
     1.7 +          // FIXME handle message range outside command range (!??!)
     1.8            val range = command.decode(raw_range).restrict(command.range)
     1.9            body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    1.10          case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)