lib/scripts/java_ext_dirs

augment Java extension directories;

#!/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 "$@"