src/Tools/JVM/java_ext_dirs
author wenzelm
Mon, 26 Mar 2012 16:25:08 +0200
changeset 47115 1a05adae1cc9
parent 47113 b5a5662528fb
child 47465 71d5f37ee2bf
permissions -rwxr-xr-x
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
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
45385
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents: 43536
diff changeset
    15
[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
43518
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    16
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    17
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    18
## main
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    19
47115
1a05adae1cc9 more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
wenzelm
parents: 47113
diff changeset
    20
isabelle_jdk java \
47113
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45385
diff changeset
    21
  -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
45385
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents: 43536
diff changeset
    22
  isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
43518
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    23