lib/scripts/java_ext_dirs
author wenzelm
Thu, 23 Jun 2011 16:10:22 +0200
changeset 43521 d477b92109b8
parent 43518 7cad71ca9bcc
child 43522 2562d6c81b03
permissions -rwxr-xr-x
provide Isabelle/Scala environment as Java extension, instead of user classpath (which is subject to adhoc changes);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43518
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     2
#
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     4
#
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     5
# Augment Java extension directories.
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     6
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     7
## diagnostics
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     8
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
     9
function fail()
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    10
{
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    11
  echo "$1" >&2
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    12
  exit 2
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    13
}
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    14
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    15
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    16
## dependencies
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    17
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    18
SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    19
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    20
TARGET_DIR="$ISABELLE_HOME/lib/classes"
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    21
TARGET="$TARGET_DIR/java_ext_dirs.jar"
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    22
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    23
if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    24
  mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    25
  pushd "$TARGET_DIR" >/dev/null
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    26
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    27
  rm -rf classes && mkdir classes
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    28
  javac -d classes -source 1.5 "$SOURCE" || fail "Failed to compile sources"
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    29
  jar cf "$(jvmpath "$TARGET")" -C classes . || fail "Failed to produce $TARGET"
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    30
  rm -rf classes
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    31
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    32
  popd >/dev/null
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    33
fi
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    34
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    35
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    36
## main
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    37
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    38
JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
43521
d477b92109b8 provide Isabelle/Scala environment as Java extension, instead of user classpath
wenzelm
parents: 43518
diff changeset
    39
exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
d477b92109b8 provide Isabelle/Scala environment as Java extension, instead of user classpath
wenzelm
parents: 43518
diff changeset
    40
  "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
43518
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    41