Position.Range: exclude singularity (again);
authorwenzelm
Thu, 02 Sep 2010 23:17:13 +0200
changeset 393426c8d0ea646a6
parent 39286 e3799716b733
child 39343 470fd769ae53
Position.Range: exclude singularity (again);
src/Pure/General/position.scala
     1.1 --- a/src/Pure/General/position.scala	Thu Sep 02 14:19:15 2010 +0200
     1.2 +++ b/src/Pure/General/position.scala	Thu Sep 02 23:17:13 2010 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4      def unapply(pos: T): Option[Text.Range] =
     1.5        (Offset.unapply(pos), End_Offset.unapply(pos)) match {
     1.6          case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
     1.7 -        case (Some(start), None) => Some(Text.Range(start))
     1.8 +        case (Some(start), None) => Some(Text.Range(start, start + 1))
     1.9          case _ => None
    1.10        }
    1.11    }