merged

--- a/lib/Tools/scala	Wed Apr 25 14:30:42 2012 +0200
+++ b/lib/Tools/scala	Wed Apr 25 15:14:57 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")" "$@"

--- a/lib/Tools/scalac	Wed Apr 25 14:30:42 2012 +0200
+++ b/lib/Tools/scalac	Wed Apr 25 15:14:57 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")" "$@"

--- a/lib/scripts/getsettings	Wed Apr 25 14:30:42 2012 +0200
+++ b/lib/scripts/getsettings	Wed Apr 25 15:14:57 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

--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 25 14:30:42 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 25 15:14:57 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
                       }
                     }
-                  */
                 }
           }
       }