author | wenzelm |
Tue, 01 Mar 2016 19:42:59 +0100 | |
changeset 62490 | 39d01eaf5292 |
parent 62036 | 773cb226738c |
child 63574 | 4ea48cbc54c1 |
permissions | -rw-r--r-- |
53483
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
2 |
# |
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
3 |
# Author: Makarius |
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
4 |
# |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
54037
diff
changeset
|
5 |
# Main Isabelle application script. |
53483
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
6 |
|
53573 | 7 |
# dereference executable |
53483
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
8 |
if [ -L "$0" ]; then |
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
9 |
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
10 |
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
11 |
fi |
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
12 |
|
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
13 |
|
53573 | 14 |
# minimal Isabelle environment |
53483
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
15 |
|
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
16 |
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)" |
53573 | 17 |
source "$ISABELLE_HOME/lib/scripts/isabelle-platform" |
53483
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
18 |
|
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
19 |
|
61134
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
20 |
# Java runtime options |
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
21 |
|
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
22 |
ISABELLE_NAME="$(basename "$0" .run)" |
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
23 |
if [ -z "$ISABELLE_PLATFORM64" ]; then |
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
24 |
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options32")) |
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
25 |
else |
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
26 |
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options64")) |
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
27 |
fi |
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
28 |
|
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
29 |
|
53573 | 30 |
# main |
53483
74a4685a96c8
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
31 |
|
54037
ab77ec347220
unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;
wenzelm
parents:
53581
diff
changeset
|
32 |
#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc. |
ab77ec347220
unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;
wenzelm
parents:
53581
diff
changeset
|
33 |
unset XMODIFIERS |
ab77ec347220
unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;
wenzelm
parents:
53581
diff
changeset
|
34 |
|
61172 | 35 |
if "$ISABELLE_HOME/bin/isabelle" jedit_client -c |
36 |
then |
|
37 |
"$ISABELLE_HOME/bin/isabelle" jedit_client "$@" |
|
38 |
else |
|
39 |
exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/jre/bin/java" \ |
|
61298 | 40 |
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ |
61172 | 41 |
-classpath "{CLASSPATH}" \ |
42 |
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \ |
|
62036 | 43 |
isabelle.Main "$@" |
61172 | 44 |
fi |