# HG changeset patch
# User wenzelm
# Date 1271529746 -7200
# Node ID 067a01827fcab2a76da66f0f2c2e5c6dad157d5b
# Parent  d4ec9ddd0e21485296ee5192df48504666e935fb
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;

diff -r d4ec9ddd0e21 -r 067a01827fca etc/settings
--- a/etc/settings	Sat Apr 17 19:35:35 2010 +0200
+++ b/etc/settings	Sat Apr 17 20:42:26 2010 +0200
@@ -55,7 +55,7 @@
 ### JVM components (Scala or Java)
 ###
 
-ISABELLE_JAVA="java"
+ISABELLE_JAVA="${THIS_JAVA:-java}"
 ISABELLE_SCALA="scala"
 
 [ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \
diff -r d4ec9ddd0e21 -r 067a01827fca src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Sat Apr 17 19:35:35 2010 +0200
+++ b/src/Pure/System/gui_setup.scala	Sat Apr 17 20:42:26 2010 +0200
@@ -56,6 +56,7 @@
     try {
       val isabelle_system = new Isabelle_System
       text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
+      text.append("Isabelle java: " + isabelle_system.this_java())
     } catch {
       case e: RuntimeException => text.append(e.getMessage + "\n")
     }
diff -r d4ec9ddd0e21 -r 067a01827fca src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Apr 17 19:35:35 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Apr 17 20:42:26 2010 +0200
@@ -26,7 +26,8 @@
   {
     import scala.collection.JavaConversions._
 
-    val env0 = Map(java.lang.System.getenv.toList: _*)
+    val env0 = Map(java.lang.System.getenv.toList: _*) +
+      ("THIS_JAVA" -> this_java())
 
     val isabelle_home =
       env0.get("ISABELLE_HOME") match {
diff -r d4ec9ddd0e21 -r 067a01827fca src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Sat Apr 17 19:35:35 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Sat Apr 17 20:42:26 2010 +0200
@@ -211,4 +211,17 @@
       }
     }
     else jvm_path
+
+
+  /* this_java executable */
+
+  def this_java(): String =
+  {
+    val java_home = System.getProperty("java.home")
+    val java_exe =
+      if (Platform.is_windows) new File(java_home + "\\bin\\java.exe")
+      else new File(java_home + "/bin/java")
+    if (!java_exe.isFile) error("Expected this Java executable: " + java_exe.toString)
+    posix_path(java_exe.getAbsolutePath)
+  }
 }