# HG changeset patch
# User wenzelm
# Date 1332617056 -3600
# Node ID b5a5662528fb9f5b401a5c56e308ff5ee9771fad
# Parent  8493d5d0e9b6bf38b87312b2a96ac59c4e4767ad
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
update for prospective jdk1.7.x component;

diff -r 8493d5d0e9b6 -r b5a5662528fb Admin/java/README
--- a/Admin/java/README	Mon Mar 26 11:15:41 2012 +0200
+++ b/Admin/java/README	Sat Mar 24 20:24:16 2012 +0100
@@ -1,2 +1,3 @@
-This is JRE 1.6.0_22 for Linux and Linux x86 from
-http://www.java.com/en/download/manual.jsp
+This is JDK 1.7.0_03 for Linux and Linux x86 from
+http://www.oracle.com/technetwork/java/javase/downloads/index.html
+
diff -r 8493d5d0e9b6 -r b5a5662528fb Admin/java/etc/settings
--- a/Admin/java/etc/settings	Mon Mar 26 11:15:41 2012 +0200
+++ b/Admin/java/etc/settings	Sat Mar 24 20:24:16 2012 +0100
@@ -1,2 +1,4 @@
-JAVA_HOME="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/jre1.6.0_22"
-ISABELLE_JAVA="$JAVA_HOME/bin/java"
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_JDK_HOME="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/jdk1.7.0_03"
+
diff -r 8493d5d0e9b6 -r b5a5662528fb NEWS
--- a/NEWS	Mon Mar 26 11:15:41 2012 +0200
+++ b/NEWS	Sat Mar 24 20:24:16 2012 +0100
@@ -45,6 +45,10 @@
 header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
 commands to be used in the same theory where defined.
 
+* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
+(not just JRE), derived from JAVA_HOME from the shell environment or
+java.home of the running JVM.
+
 
 *** Pure ***
 
diff -r 8493d5d0e9b6 -r b5a5662528fb etc/settings
--- a/etc/settings	Mon Mar 26 11:15:41 2012 +0200
+++ b/etc/settings	Sat Mar 24 20:24:16 2012 +0100
@@ -54,10 +54,12 @@
 ### JVM components (Scala or Java)
 ###
 
-if [ -n "$JAVA_HOME" ]; then
-  ISABELLE_JAVA="$JAVA_HOME/bin/java"
-else
-  ISABELLE_JAVA="java"
+if [ -z "$ISABELLE_JDK_HOME" -a -n "$JAVA_HOME" ]; then
+  if [ "$(basename "$JAVA_HOME")" = jre -a -e "$(dirname "$JAVA_HOME")"/bin/javac ]; then
+    ISABELLE_JDK_HOME="$(dirname "$JAVA_HOME")"
+  else
+    ISABELLE_JDK_HOME="$JAVA_HOME"
+  fi
 fi
 
 ISABELLE_SCALA_BUILD_OPTIONS="-nowarn -target:jvm-1.5"
diff -r 8493d5d0e9b6 -r b5a5662528fb lib/Tools/java
--- a/lib/Tools/java	Mon Mar 26 11:15:41 2012 +0200
+++ b/lib/Tools/java	Sat Mar 24 20:24:16 2012 +0100
@@ -6,7 +6,7 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 
-JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+JAVA_EXE="$ISABELLE_JDK_HOME/bin/java"
 
 if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
   :
diff -r 8493d5d0e9b6 -r b5a5662528fb lib/browser/build
--- a/lib/browser/build	Mon Mar 26 11:15:41 2012 +0200
+++ b/lib/browser/build	Sat Mar 24 20:24:16 2012 +0100
@@ -65,9 +65,9 @@
 
   rm -rf classes && mkdir classes
 
-  javac -d classes -source 1.4 "${SOURCES[@]}" || \
+  "$ISABELLE_JDK_HOME/bin/javac" -d classes -source 1.4 "${SOURCES[@]}" || \
     fail "Failed to compile sources"
-  jar cf "$(jvmpath "$TARGET")" -C classes . ||
+  "$ISABELLE_JDK_HOME/bin/jar" cf "$(jvmpath "$TARGET")" -C classes . ||
     fail "Failed to produce $TARGET"
 
   rm -rf classes
diff -r 8493d5d0e9b6 -r b5a5662528fb src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Mon Mar 26 11:15:41 2012 +0200
+++ b/src/Pure/System/gui_setup.scala	Sat Mar 24 20:24:16 2012 +0100
@@ -43,6 +43,7 @@
       text.append("Cygwin root: " + Cygwin.check_root() + "\n")
     text.append("JVM name: " + Platform.jvm_name + "\n")
     text.append("JVM platform: " + Platform.jvm_platform + "\n")
+    text.append("JVM home: " + java.lang.System.getProperty("java.home") + "\n")
     try {
       Isabelle_System.init()
       text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
@@ -50,7 +51,7 @@
       val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
       if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
       text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
-      text.append("Isabelle java: " + Isabelle_System.getenv("THIS_JAVA") + "\n")
+      text.append("Isabelle jdk home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
     }
     catch { case ERROR(msg) => text.append(msg + "\n") }
 
diff -r 8493d5d0e9b6 -r b5a5662528fb src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 26 11:15:41 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Mar 24 20:24:16 2012 +0100
@@ -51,7 +51,7 @@
       val settings =
       {
         val env = Map(System.getenv.toList: _*) +
-          ("THIS_JAVA" -> standard_system.this_java())
+          ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home())
 
         val isabelle_home =
           if (this_isabelle_home != null) this_isabelle_home
diff -r 8493d5d0e9b6 -r b5a5662528fb src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Mar 26 11:15:41 2012 +0200
+++ b/src/Pure/System/standard_system.scala	Sat Mar 24 20:24:16 2012 +0100
@@ -333,15 +333,17 @@
     else jvm_path
 
 
-  /* this_java executable */
+  /* JDK home of running JVM */
 
-  def this_java(): String =
+  def this_jdk_home(): 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)
+    val home = new File(java_home)
+    val parent = home.getParent
+    val jdk_home =
+      if (home.getName == "jre" && parent != null &&
+          (new File(new File(parent, "bin"), "javac")).exists) parent
+      else java_home
+    posix_path(jdk_home)
   }
 }
diff -r 8493d5d0e9b6 -r b5a5662528fb src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Mar 26 11:15:41 2012 +0200
+++ b/src/Pure/build-jars	Sat Mar 24 20:24:16 2012 +0100
@@ -186,7 +186,7 @@
   mkdir -p "$(dirname "$CHARSET_SERVICE")"
   echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"
 
-  jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
+  "$ISABELLE_JDK_HOME/bin/jar" cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
     fail "Failed to produce $TARGET"
 
   cp "$SCALA_HOME/lib/scala-swing.jar" "$SCALA_HOME/lib/scala-library.jar" "$TARGET_DIR/ext"
diff -r 8493d5d0e9b6 -r b5a5662528fb src/Tools/JVM/java_ext_dirs
--- a/src/Tools/JVM/java_ext_dirs	Mon Mar 26 11:15:41 2012 +0200
+++ b/src/Tools/JVM/java_ext_dirs	Sat Mar 24 20:24:16 2012 +0100
@@ -17,7 +17,7 @@
 
 ## main
 
-JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
+exec "$ISABELLE_JDK_HOME/bin/java" \
+  -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
   isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
 
diff -r 8493d5d0e9b6 -r b5a5662528fb src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Mar 26 11:15:41 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Mar 24 20:24:16 2012 +0100
@@ -248,7 +248,7 @@
   ) || fail "Failed to compile sources"
 
   cd dist/classes
-  jar cf "../jars/Isabelle-jEdit.jar" * || failed
+  "$ISABELLE_JDK_HOME/bin/jar" cf "../jars/Isabelle-jEdit.jar" * || failed
   cd ../..
   rm -rf dist/classes
 fi