# HG changeset patch
# User wenzelm
# Date 1320674398 -3600
# Node ID 7c1375ba142478742c4049eb3fe912689eaf5691
# Parent  dffa657f0aa21e1d03a42de5032f3360c3097fa3
offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;

diff -r dffa657f0aa2 -r 7c1375ba1424 Admin/build
--- a/Admin/build	Mon Nov 07 14:23:50 2011 +0100
+++ b/Admin/build	Mon Nov 07 14:59:58 2011 +0100
@@ -84,7 +84,6 @@
 
 function build_jars ()
 {
-  "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
   popd >/dev/null
diff -r dffa657f0aa2 -r 7c1375ba1424 lib/Tools/java
--- a/lib/Tools/java	Mon Nov 07 14:23:50 2011 +0100
+++ b/lib/Tools/java	Mon Nov 07 14:59:58 2011 +0100
@@ -22,5 +22,5 @@
 fi
 
 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
 
diff -r dffa657f0aa2 -r 7c1375ba1424 lib/Tools/scala
--- a/lib/Tools/scala	Mon Nov 07 14:23:50 2011 +0100
+++ b/lib/Tools/scala	Mon Nov 07 14:59:58 2011 +0100
@@ -10,4 +10,4 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
diff -r dffa657f0aa2 -r 7c1375ba1424 lib/Tools/scalac
--- a/lib/Tools/scalac	Mon Nov 07 14:23:50 2011 +0100
+++ b/lib/Tools/scalac	Mon Nov 07 14:59:58 2011 +0100
@@ -10,4 +10,4 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
diff -r dffa657f0aa2 -r 7c1375ba1424 lib/scripts/java_ext_dirs
--- a/lib/scripts/java_ext_dirs	Mon Nov 07 14:23:50 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Augment Java extension directories.
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## dependencies
-
-SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
-
-TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/java_ext_dirs.jar"
-
-if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
-  mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
-  pushd "$TARGET_DIR" >/dev/null
-
-  BUILD="build$$"
-  TMP_JAR="java_ext_dirs$$.jar"
-
-  rm -rf "$BUILD" && mkdir "$BUILD"
-  javac -d "$BUILD" -source 1.5 "$(jvmpath "$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"
-
-  popd >/dev/null
-fi
-
-
-## main
-
-JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
-  "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
-
diff -r dffa657f0aa2 -r 7c1375ba1424 src/Pure/System/Java_Ext_Dirs.java
--- a/src/Pure/System/Java_Ext_Dirs.java	Mon Nov 07 14:23:50 2011 +0100
+++ /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 dffa657f0aa2 -r 7c1375ba1424 src/Tools/JVM/Java_Ext_Dirs.java
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/Java_Ext_Dirs.java	Mon Nov 07 14:59:58 2011 +0100
@@ -0,0 +1,22 @@
+/*  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 dffa657f0aa2 -r 7c1375ba1424 src/Tools/JVM/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/build	Mon Nov 07 14:59:58 2011 +0100
@@ -0,0 +1,31 @@
+#!/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 dffa657f0aa2 -r 7c1375ba1424 src/Tools/JVM/java_ext_dirs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/java_ext_dirs	Mon Nov 07 14:59:58 2011 +0100
@@ -0,0 +1,23 @@
+#!/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
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
+  isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
+
diff -r dffa657f0aa2 -r 7c1375ba1424 src/Tools/JVM/java_ext_dirs.jar
Binary file src/Tools/JVM/java_ext_dirs.jar has changed