merged

--- a/src/HOL/Nat.thy	Thu Jun 18 11:52:37 2009 -0700
+++ b/src/HOL/Nat.thy	Thu Jun 18 12:00:03 2009 -0700
@@ -849,17 +849,20 @@
 lemma less_Suc_induct:
   assumes less:  "i < j"
      and  step:  "!!i. P i (Suc i)"
-     and  trans: "!!i j k. P i j ==> P j k ==> P i k"
+     and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
   shows "P i j"
 proof -
-  from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add)
+  from less obtain k where j: "j = Suc (i + k)" by (auto dest: less_imp_Suc_add)
   have "P i (Suc (i + k))"
   proof (induct k)
     case 0
     show ?case by (simp add: step)
   next
     case (Suc k)
-    thus ?case by (auto intro: assms)
+    have "0 + i < Suc k + i" by (rule add_less_mono1) simp
+    hence "i < Suc (i + k)" by (simp add: add_commute)
+    from trans[OF this lessI Suc step]
+    show ?case by simp
   qed
   thus "P i j" by (simp add: j)
 qed

--- a/src/Pure/General/position.scala	Thu Jun 18 11:52:37 2009 -0700
+++ b/src/Pure/General/position.scala	Thu Jun 18 12:00:03 2009 -0700
@@ -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 11:52:37 2009 -0700
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 18 12:00:03 2009 -0700
@@ -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 }
   }