src/Tools/JVM/java_ext_dirs
author blanchet
Tue, 10 Jul 2012 23:36:03 +0200
changeset 48226 76759312b0b4
parent 47878 45bfbd7d6e58
permissions -rwxr-xr-x
generate deep terms as feature
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
47878
45bfbd7d6e58 file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;
wenzelm
parents: 47465
diff changeset
    20
isabelle_jdk java -Dfile.encoding=UTF-8 \
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")" \
47465
71d5f37ee2bf more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents: 47115
diff changeset
    22
  isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null
43518
7cad71ca9bcc augment Java extension directories;
wenzelm
parents:
diff changeset
    23