| author | wenzelm |
| Fri, 10 Jan 2020 16:37:47 +0100 | |
| changeset 71363 | ce3409dfb18c |
| parent 71338 | Admin/Linux/Isabelle.run@373dcdd363dc |
| child 71459 | 4876e6f62fe5 |
| permissions | -rwxr-xr-x |
|
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 |
# 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
|
8 |
|
| 71338 | 9 |
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)" |
| 53573 | 10 |
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
|
11 |
|
|
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 |
|
|
61134
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
13 |
# Java runtime options |
|
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
14 |
|
|
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
15 |
ISABELLE_NAME="$(basename "$0" .run)" |
|
67492
954f44210b92
options file for x86_64 only (amending 03a96b8c7c06);
wenzelm
parents:
67490
diff
changeset
|
16 |
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options"))
|
|
61134
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
17 |
|
|
80ac5e17772d
clarified Java runtime options for 32 vs. 64 bit;
wenzelm
parents:
58792
diff
changeset
|
18 |
|
| 53573 | 19 |
# 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
|
20 |
|
|
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
|
21 |
#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
|
22 |
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
|
23 |
|
|
67492
954f44210b92
options file for x86_64 only (amending 03a96b8c7c06);
wenzelm
parents:
67490
diff
changeset
|
24 |
exec "$ISABELLE_HOME/contrib/jdk/x86_64-linux/jre/bin/java" \ |
|
63574
4ea48cbc54c1
uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly;
wenzelm
parents:
62036
diff
changeset
|
25 |
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
|
|
4ea48cbc54c1
uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly;
wenzelm
parents:
62036
diff
changeset
|
26 |
-classpath "{CLASSPATH}" \
|
|
4ea48cbc54c1
uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly;
wenzelm
parents:
62036
diff
changeset
|
27 |
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \ |
|
4ea48cbc54c1
uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly;
wenzelm
parents:
62036
diff
changeset
|
28 |
isabelle.Main "$@" |