# HG changeset patch # User wenzelm # Date 1335362076 -7200 # Node ID af40c7e90c1e08bc2f22887fe493e251e46ba747 # Parent 5e6fe71e2390c0fef77be921b566e091da090bb7# Parent 8c37cb84065f0853e9f9e3c5a4a1ff7a7bef5dc5 merged diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/isatest/settings/at-poly --- a/Admin/isatest/settings/at-poly Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/isatest/settings/at-poly Wed Apr 25 15:54:36 2012 +0200 @@ -24,6 +24,5 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true" -init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/isatest/settings/at-poly-e --- a/Admin/isatest/settings/at-poly-e Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/isatest/settings/at-poly-e Wed Apr 25 15:54:36 2012 +0200 @@ -24,5 +24,4 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true" -init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/isatest/settings/at-poly-test --- a/Admin/isatest/settings/at-poly-test Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/isatest/settings/at-poly-test Wed Apr 25 15:54:36 2012 +0200 @@ -28,5 +28,4 @@ ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml" ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl" -init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/isatest/settings/at64-poly --- a/Admin/isatest/settings/at64-poly Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/isatest/settings/at64-poly Wed Apr 25 15:54:36 2012 +0200 @@ -24,5 +24,4 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" -init_component "$HOME/contrib_devel/jdk-7u3_x86_64-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/isatest/settings/cygwin-poly-e --- a/Admin/isatest/settings/cygwin-poly-e Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/isatest/settings/cygwin-poly-e Wed Apr 25 15:54:36 2012 +0200 @@ -24,5 +24,4 @@ ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false" -init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib/kodkodi-1.2.16" diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/java/README --- a/Admin/java/README Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/java/README Wed Apr 25 15:54:36 2012 +0200 @@ -1,3 +1,3 @@ -This is JDK 1.7.0_03 for Linux from +This is JDK 1.6.0_31 for Linux from http://www.oracle.com/technetwork/java/javase/downloads/index.html diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/java/etc/settings --- a/Admin/java/etc/settings Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/java/etc/settings Wed Apr 25 15:54:36 2012 +0200 @@ -1,4 +1,4 @@ # -*- shell-script -*- :mode=shellscript: -ISABELLE_JDK_HOME="$COMPONENT/jdk1.7.0_03" +ISABELLE_JDK_HOME="$COMPONENT/jdk1.6.0_31" diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/launch4j/Isabelle.exe Binary file Admin/launch4j/Isabelle.exe has changed diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/launch4j/README --- a/Admin/launch4j/README Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/launch4j/README Wed Apr 25 15:54:36 2012 +0200 @@ -1,5 +1,4 @@ -Cross-platform Java executable wrapper -====================================== +Java application wrapper for Windows +==================================== * http://launch4j.sourceforge.net - diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/launch4j/isabelle.xml --- a/Admin/launch4j/isabelle.xml Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/launch4j/isabelle.xml Wed Apr 25 15:54:36 2012 +0200 @@ -20,7 +20,7 @@ lib\classes\ext\scala-swing.jar - contrib\jdk-7u3_x86-cygwin\jdk1.7.0_03 + contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31 jdkOnly diff -r 5e6fe71e2390 -r af40c7e90c1e Admin/mira.py --- a/Admin/mira.py Wed Apr 25 15:09:18 2012 +0200 +++ b/Admin/mira.py Wed Apr 25 15:54:36 2012 +0200 @@ -59,7 +59,6 @@ ISABELLE_USEDIR_OPTIONS="%s" -ISABELLE_JDK_HOME="$JAVA_HOME" Z3_NON_COMMERCIAL="yes" %s diff -r 5e6fe71e2390 -r af40c7e90c1e README --- a/README Wed Apr 25 15:09:18 2012 +0200 +++ b/README Wed Apr 25 15:54:36 2012 +0200 @@ -16,7 +16,7 @@ * The Poly/ML compiler and runtime system (version 5.2.1 or later). * The GNU bash shell (version 3.x or 2.x). * Perl (version 5.x). - * Java 1.6.x or 1.7.x from Oracle or Apple -- for Scala and jEdit. + * Java 1.6.x from Oracle or Apple -- for Scala and jEdit. * GNU Emacs (version 23 or 24) -- for the Proof General 4.x interface. * A complete LaTeX installation -- for document preparation. diff -r 5e6fe71e2390 -r af40c7e90c1e etc/settings --- a/etc/settings Wed Apr 25 15:09:18 2012 +0200 +++ b/etc/settings Wed Apr 25 15:54:36 2012 +0200 @@ -140,11 +140,14 @@ # The pdf file viewer case "$ISABELLE_PLATFORM" in + *-linux) + PDF_VIEWER="xdg-open" + ;; *-darwin) PDF_VIEWER="open -W -n" ;; - *) - PDF_VIEWER=evince + *-cygwin) + PDF_VIEWER="cygstart" ;; esac diff -r 5e6fe71e2390 -r af40c7e90c1e lib/Tools/scala --- a/lib/Tools/scala Wed Apr 25 15:09:18 2012 +0200 +++ b/lib/Tools/scala Wed Apr 25 15:54:36 2012 +0200 @@ -6,8 +6,6 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } -export JAVA_HOME="$ISABELLE_JDK_HOME" - CLASSPATH="$(jvmpath "$CLASSPATH")" isabelle_scala scala -Dfile.encoding=UTF-8 \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r 5e6fe71e2390 -r af40c7e90c1e lib/Tools/scalac --- a/lib/Tools/scalac Wed Apr 25 15:09:18 2012 +0200 +++ b/lib/Tools/scalac Wed Apr 25 15:54:36 2012 +0200 @@ -6,8 +6,6 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } -export JAVA_HOME="$ISABELLE_JDK_HOME" - CLASSPATH="$(jvmpath "$CLASSPATH")" isabelle_scala scalac -Dfile.encoding=UTF-8 \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r 5e6fe71e2390 -r af40c7e90c1e lib/scripts/getsettings --- a/lib/scripts/getsettings Wed Apr 25 15:09:18 2012 +0200 +++ b/lib/scripts/getsettings Wed Apr 25 15:54:36 2012 +0200 @@ -203,6 +203,9 @@ ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" fi +#enforce JAVA_HOME +export JAVA_HOME="$ISABELLE_JDK_HOME" + ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" set +o allexport diff -r 5e6fe71e2390 -r af40c7e90c1e src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 25 15:09:18 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 25 15:54:36 2012 +0200 @@ -180,7 +180,7 @@ (length ts downto 1) ts))] fun install_java_message () = - "Nitpick requires Java Development Kit 1.6/1.7 via ISABELLE_JDK_HOME setting." + "Nitpick requires Java Development Kit 1.6 via ISABELLE_JDK_HOME setting." fun install_kodkodi_message () = "Nitpick requires the external Java program Kodkodi. To install it, download \ \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \ diff -r 5e6fe71e2390 -r af40c7e90c1e src/Tools/jEdit/README_BUILD --- a/src/Tools/jEdit/README_BUILD Wed Apr 25 15:09:18 2012 +0200 +++ b/src/Tools/jEdit/README_BUILD Wed Apr 25 15:54:36 2012 +0200 @@ -1,10 +1,10 @@ Requirements for instantaneous build from sources ================================================= -* Official Java JDK 1.6/1.7 from Sun/Oracle/Apple +* Official Java JDK 1.6 from Sun/Oracle/Apple http://www.oracle.com/technetwork/java/javase/downloads/index.html - (or OpenJDK 1.7, but not OpenJDK 1.6) + (experimental support for JDK/OpenJDK 1.7, but not OpenJDK 1.6) * Scala 2.9.2 (or 2.8.2.final) http://www.scala-lang.org diff -r 5e6fe71e2390 -r af40c7e90c1e src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 25 15:09:18 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 25 15:54:36 2012 +0200 @@ -105,14 +105,12 @@ if (ds.isEmpty) null else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { - /* FIXME Java 7 only override def getRenderer() = - new ListCellRenderer[Any] { - val default_renderer = - (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]] + new ListCellRenderer { + val default_renderer = new DefaultListCellRenderer override def getListCellRendererComponent( - list: JList[_ <: Any], value: Any, index: Int, + list: JList, value: Any, index: Int, selected: Boolean, focus: Boolean): Component = { val renderer: Component = @@ -122,7 +120,6 @@ renderer } } - */ } } }