# HG changeset patch
# User wenzelm
# Date 1245344619 -7200
# Node ID 0c83e3e75fcf2ab3d6dcce0fe96ff7c2899443cb
# Parent  b8628ac68b73caf8c37ae241b978311dbfe07cb0
replaced java Properties by pure property lists;
added offsets_of;

diff -r b8628ac68b73 -r 0c83e3e75fcf src/Pure/General/position.scala
--- 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))
+  }
+
 }