src/Pure/General/position.scala
changeset 39041 6c8d0ea646a6
parent 38887 1261481ef5e5
child 41483 4a8431c73cf2
--- a/src/Pure/General/position.scala	Thu Sep 02 14:19:15 2010 +0200
+++ b/src/Pure/General/position.scala	Thu Sep 02 23:17:13 2010 +0200
@@ -24,7 +24,7 @@
     def unapply(pos: T): Option[Text.Range] =
       (Offset.unapply(pos), End_Offset.unapply(pos)) match {
         case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
-        case (Some(start), None) => Some(Text.Range(start))
+        case (Some(start), None) => Some(Text.Range(start, start + 1))
         case _ => None
       }
   }