# HG changeset patch
# User wenzelm
# Date 1345749794 -7200
# Node ID 34fac6fb9b032b91e93f66b3d5b8001a4e58d4fc
# Parent  51560e392e1b2c8c5a1d2fe31fadc948457c93bf
simplified JVM startup, based on stronger assumptions about the Java version provided as Isabelle component;

diff -r 51560e392e1b -r 34fac6fb9b03 lib/Tools/java
--- a/lib/Tools/java	Thu Aug 23 20:49:00 2012 +0200
+++ b/lib/Tools/java	Thu Aug 23 21:23:14 2012 +0200
@@ -5,13 +5,6 @@
 # DESCRIPTION: invoke Java within the Isabelle environment
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
+isabelle_jdk java -Dfile.encoding=UTF-8 -server \
+  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
 
-if isabelle_jdk java -server >/dev/null 2>/dev/null; then
-  SERVER="-server"
-else
-  SERVER=""
-fi
-
-isabelle_jdk java -Dfile.encoding=UTF-8 $SERVER \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
-
diff -r 51560e392e1b -r 34fac6fb9b03 lib/Tools/scala
--- a/lib/Tools/scala	Thu Aug 23 20:49:00 2012 +0200
+++ b/lib/Tools/scala	Thu Aug 23 21:23:14 2012 +0200
@@ -8,4 +8,4 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 isabelle_scala scala -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
diff -r 51560e392e1b -r 34fac6fb9b03 lib/Tools/scalac
--- a/lib/Tools/scalac	Thu Aug 23 20:49:00 2012 +0200
+++ b/lib/Tools/scalac	Thu Aug 23 21:23:14 2012 +0200
@@ -8,4 +8,5 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 isabelle_scala scalac -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+
diff -r 51560e392e1b -r 34fac6fb9b03 src/Tools/JVM/Java_Ext_Dirs.java
--- a/src/Tools/JVM/Java_Ext_Dirs.java	Thu Aug 23 20:49:00 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-/*  Title:      Pure/System/Java_Ext_Dirs.java
-    Author:     Makarius
-
-Augment Java extension directories.
-*/
-
-package isabelle;
-
-public class Java_Ext_Dirs
-{
-  public static void main(String [] args) {
-    StringBuilder s = new StringBuilder();
-    int i;
-    for (i = 0; i < args.length; i++) {
-      s.append(args[i]);
-      s.append(System.getProperty("path.separator"));
-    }
-    s.append(System.getProperty("java.ext.dirs"));
-    System.out.println(s.toString());
-  }
-}
-
diff -r 51560e392e1b -r 34fac6fb9b03 src/Tools/JVM/build
--- a/src/Tools/JVM/build	Thu Aug 23 20:49:00 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Offline build script for JVM tools.
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## build
-
-cd "$(dirname "$0")"
-
-SOURCE="Java_Ext_Dirs.java"
-TARGET="java_ext_dirs.jar"
-
-BUILD="build_dir$$"
-TMP_JAR="java_ext_dirs$$.jar"
-
-rm -rf "$BUILD" && mkdir "$BUILD"
-javac -source 1.4 -target 1.4 -d "$BUILD" "$SOURCE" || fail "Failed to compile sources"
-jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce \"$TMP_JAR\""
-mv "$TMP_JAR" "$TARGET"
-rm -rf "$BUILD"
-
diff -r 51560e392e1b -r 34fac6fb9b03 src/Tools/JVM/java_ext_dirs
--- a/src/Tools/JVM/java_ext_dirs	Thu Aug 23 20:49:00 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Augment Java extension directories.
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
-
-
-## main
-
-isabelle_jdk java -Dfile.encoding=UTF-8 \
-  -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
-  isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null
-
diff -r 51560e392e1b -r 34fac6fb9b03 src/Tools/JVM/java_ext_dirs.jar
Binary file src/Tools/JVM/java_ext_dirs.jar has changed