merged

--- a/src/Pure/General/position.scala	Thu Jun 18 08:45:26 2009 -0700
+++ b/src/Pure/General/position.scala	Thu Jun 18 19:10:22 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))
+  }
+
 }

--- a/src/Pure/System/isabelle_system.scala	Thu Jun 18 08:45:26 2009 -0700
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 18 19:10:22 2009 +0200
@@ -98,7 +98,9 @@
           if (i <= 0) (entry -> "")
           else (entry.substring(0, i) -> entry.substring(i + 1))
         }
-      Map(entries: _*)
+      Map(entries: _*) +
+        ("HOME" -> java.lang.System.getenv("HOME")) +
+        ("PATH" -> java.lang.System.getenv("PATH"))
     }
     finally { dump.delete }
   }