# HG changeset patch
# User wenzelm
# Date 1308828180 -7200
# Node ID 7cad71ca9bcc031bb02e5406cb0e6e69c2221561
# Parent  87ec9a1c0f98201e7ddf1822cd2f93063255db18
augment Java extension directories;

diff -r 87ec9a1c0f98 -r 7cad71ca9bcc lib/scripts/java_ext_dirs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/java_ext_dirs	Thu Jun 23 13:23:00 2011 +0200
@@ -0,0 +1,40 @@
+#!/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
+
+  rm -rf classes && mkdir classes
+  javac -d classes -source 1.5 "$SOURCE" || fail "Failed to compile sources"
+  jar cf "$(jvmpath "$TARGET")" -C classes . || fail "Failed to produce $TARGET"
+  rm -rf classes
+
+  popd >/dev/null
+fi
+
+
+## main
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs "$@"
+
diff -r 87ec9a1c0f98 -r 7cad71ca9bcc src/Pure/System/Java_Ext_Dirs.java
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/Java_Ext_Dirs.java	Thu Jun 23 13:23:00 2011 +0200
@@ -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();
+    s.append(System.getProperty("java.ext.dirs"));
+    int i;
+    for (i = 0; i < args.length; i++) {
+      s.append(System.getProperty("path.separator"));
+      s.append(args[i]);
+    }
+    System.out.println(s.toString());
+  }
+}
+