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 }