improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;

--- 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 \

--- 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")
     }

--- 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 {

--- 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)
+  }
 }