--- a/src/Pure/General/position.scala Wed Aug 25 21:31:22 2010 +0200
+++ b/src/Pure/General/position.scala Wed Aug 25 22:37:53 2010 +0200
@@ -11,22 +11,21 @@
{
type T = List[(String, String)]
- def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
- def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
- def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
- def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
- def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
- def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
- 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)
+ val Line = new Markup.Int_Property(Markup.LINE)
+ val End_Line = new Markup.Int_Property(Markup.END_LINE)
+ val Offset = new Markup.Int_Property(Markup.OFFSET)
+ val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
+ val File = new Markup.Property(Markup.FILE)
+ val Id = new Markup.Long_Property(Markup.ID)
- def get_range(pos: T): Option[Text.Range] =
- (get_offset(pos), get_end_offset(pos)) match {
- case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
- case (Some(start), None) => Some(Text.Range(start))
- case (_, _) => None
- }
-
- object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
- object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
+ object Range
+ {
+ def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
+ 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 _ => None
+ }
+ }
}