--- a/src/Pure/General/position.scala Thu Jun 18 17:22:41 2009 +0200
+++ b/src/Pure/General/position.scala Thu Jun 18 19:03:39 2009 +0200
@@ -11,13 +11,14 @@
object Position {
- private def get_string(name: String, props: Properties) = {
- val value = if (props != null) props.getProperty(name) else null
- if (value != null) Some(value) else None
- }
+ type T = List[(String, String)]
- private def get_int(name: String, props: Properties) = {
- get_string(name, props) match {
+ private def get_string(name: String, pos: T): Option[String] =
+ pos.find(p => p._1 == name).map(_._2)
+
+ private def get_int(name: String, pos: T): Option[Int] =
+ {
+ get_string(name, pos) match {
case None => None
case Some(value) =>
try { Some(Integer.parseInt(value)) }
@@ -25,12 +26,20 @@
}
}
- def line_of(props: Properties) = get_int(Markup.LINE, props)
- def column_of(props: Properties) = get_int(Markup.COLUMN, props)
- def offset_of(props: Properties) = get_int(Markup.OFFSET, props)
- def end_line_of(props: Properties) = get_int(Markup.END_LINE, props)
- def end_column_of(props: Properties) = get_int(Markup.END_COLUMN, props)
- def end_offset_of(props: Properties) = get_int(Markup.END_OFFSET, props)
- def file_of(props: Properties) = get_string(Markup.FILE, props)
- def id_of(props: Properties) = get_string(Markup.ID, props)
+ def line_of(pos: T) = get_int(Markup.LINE, pos)
+ def column_of(pos: T) = get_int(Markup.COLUMN, pos)
+ def offset_of(pos: T) = get_int(Markup.OFFSET, pos)
+ def end_line_of(pos: T) = get_int(Markup.END_LINE, pos)
+ def end_column_of(pos: T) = get_int(Markup.END_COLUMN, pos)
+ def end_offset_of(pos: T) = get_int(Markup.END_OFFSET, pos)
+ def file_of(pos: T) = get_string(Markup.FILE, pos)
+ def id_of(pos: T) = get_string(Markup.ID, pos)
+
+ def offsets_of(pos: T): (Option[Int], Option[Int]) =
+ {
+ val begin = offset_of(pos)
+ val end = end_offset_of(pos)
+ (begin, if (end.isDefined) end else begin.map(_ + 1))
+ }
+
}