src/Pure/General/position.scala

--- a/src/Pure/General/position.scala	Thu May 06 15:04:37 2010 +0200
+++ b/src/Pure/General/position.scala	Thu May 06 16:27:47 2010 +0200
@@ -11,27 +11,14 @@
 {
   type T = List[(String, String)]
 
-  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)) }
-        catch { case _: NumberFormatException => None }
-    }
-  }
-
-  def get_line(pos: T): Option[Int] = get_int(Markup.LINE, pos)
-  def get_column(pos: T): Option[Int] = get_int(Markup.COLUMN, pos)
-  def get_offset(pos: T): Option[Int] = get_int(Markup.OFFSET, pos)
-  def get_end_line(pos: T): Option[Int] = get_int(Markup.END_LINE, pos)
-  def get_end_column(pos: T): Option[Int] = get_int(Markup.END_COLUMN, pos)
-  def get_end_offset(pos: T): Option[Int] = get_int(Markup.END_OFFSET, pos)
-  def get_file(pos: T): Option[String] = get_string(Markup.FILE, pos)
-  def get_id(pos: T): Option[String] = get_string(Markup.ID, pos)
+  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[String] = Markup.get_string(Markup.ID, pos)
 
   def get_range(pos: T): Option[(Int, Int)] =
     (get_offset(pos), get_end_offset(pos)) match {