src/Pure/General/position.scala

--- a/src/Pure/General/position.scala	Wed Aug 18 14:04:13 2010 +0200
+++ b/src/Pure/General/position.scala	Wed Aug 18 23:44:50 2010 +0200
@@ -20,13 +20,13 @@
   def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
   def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
 
-  def get_range(pos: T): Option[(Int, Int)] =
+  def get_range(pos: T): Option[Text.Range] =
     (get_offset(pos), get_end_offset(pos)) match {
-      case (Some(begin), Some(end)) => Some(begin, end)
-      case (Some(begin), None) => Some(begin, begin + 1)
+      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
+      case (Some(start), None) => Some(Text.Range(start, start + 1))
       case (None, _) => None
     }
 
   object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
-  object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
+  object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
 }