lib/scripts/java_ext_dirs

tune indenting

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