1.1 --- a/src/Pure/General/position.scala	Thu Aug 19 22:52:00 2010 +0200
     1.2 +++ b/src/Pure/General/position.scala	Fri Aug 20 11:00:15 2010 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4  
     1.5    def get_range(pos: T): Option[Text.Range] =
     1.6      (get_offset(pos), get_end_offset(pos)) match {
     1.7 -      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
     1.8 -      case (Some(start), None) => Some(Text.Range(start, start + 1))
     1.9 -      case (None, _) => None
    1.10 +      case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
    1.11 +      case (Some(start), None) => Some(Text.Range(start, start))
    1.12 +      case (_, _) => None
    1.13      }
    1.14  
    1.15    object Id { def unapply(pos: T): Option[Long] = get_id(pos) }