src/Pure/PIDE/protocol.scala
changeset 55822 ccf2d784be97
parent 55820 61869776ce1f
child 55884 f2c0eaedd579
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Mar 01 13:05:46 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Mar 01 15:58:47 2014 +0100
     1.3 @@ -289,8 +289,8 @@
     1.4        props match {
     1.5          case Position.Reported(id, file_name, raw_range)
     1.6          if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
     1.7 -          chunk.decode(raw_range).try_restrict(chunk.range) match {
     1.8 -            case Some(range) if !range.is_singularity => set + range
     1.9 +          chunk.incorporate(raw_range) match {
    1.10 +            case Some(range) => set + range
    1.11              case _ => set
    1.12            }
    1.13          case _ => set