--- a/src/Pure/General/position.scala Thu Aug 19 22:52:00 2010 +0200
+++ b/src/Pure/General/position.scala Fri Aug 20 11:00:15 2010 +0200
@@ -22,9 +22,9 @@
def get_range(pos: T): Option[Text.Range] =
(get_offset(pos), get_end_offset(pos)) match {
- case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
- case (Some(start), None) => Some(Text.Range(start, start + 1))
- case (None, _) => None
+ case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
+ case (Some(start), None) => Some(Text.Range(start, start))
+ case (_, _) => None
}
object Id { def unapply(pos: T): Option[Long] = get_id(pos) }