src/Pure/General/position.scala

--- 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) }