# HG changeset patch
# User wenzelm
# Date 1219525656 -7200
# Node ID 85b5f024d94b017c062981c6e096d6a6bf87abcf
# Parent  4a34af0f8cee9d73381802b288b98ca19742e73c
Position properties.

diff -r 4a34af0f8cee -r 85b5f024d94b src/Pure/General/position.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/position.scala	Sat Aug 23 23:07:36 2008 +0200
@@ -0,0 +1,37 @@
+/*  Title:      Pure/General/position.scala
+    ID:         $Id$
+    Author:     Makarius
+
+Position properties.
+*/
+
+package isabelle
+
+import java.util.Properties
+
+
+object Position {
+
+  private def get_string(name: String, props: Properties) = {
+    val value = props.getProperty(name)
+    if (value != null) Some(value) else None
+  }
+
+  private def get_int(name: String, props: Properties) = {
+    get_string(name, props) match {
+      case None => None
+      case Some(value) =>
+        try { Some(Integer.parseInt(value)) }
+        catch { case e: NumberFormatException => None }
+    }
+  }
+
+  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)
+}