# 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
}
}
- */
}
}
}