# HG changeset patch
# User wenzelm
# Date 1283462233 -7200
# Node ID 6c8d0ea646a635ac9b96342bf80a5f44b42235ec
# Parent  e3799716b73321788054dec7b1b1269e6d302a74
Position.Range: exclude singularity (again);

diff -r e3799716b733 -r 6c8d0ea646a6 src/Pure/General/position.scala
--- 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
       }
   }