author | wenzelm |
Mon, 07 Dec 2020 19:22:37 +0100 | |
changeset 72845 | 60f56f623be2 |
parent 69126 | e1b4b14ded58 |
child 73705 | ac07f6be27ea |
permissions | -rwxr-xr-x |
63995 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# Author: Makarius |
|
4 |
# |
|
5 |
# Isabelle/Java cold start -- without settings environment |
|
6 |
||
7 |
if [ -L "$0" ]; then |
|
8 |
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
|
9 |
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
|
10 |
fi |
|
11 |
||
12 |
export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
|
13 |
||
14 |
( |
|
15 |
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
|
16 |
||
66906 | 17 |
eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $ISABELLE_TOOL_JAVA_OPTIONS)" |
63995 | 18 |
|
19 |
if [ -f "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" ]; then |
|
20 |
classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" |
|
21 |
fi |
|
22 |
||
23 |
[ -n "$CLASSPATH" ] && classpath "$CLASSPATH" |
|
24 |
||
25 |
echo "$ISABELLE_ROOT" |
|
26 |
echo "$CYGWIN_ROOT" |
|
27 |
echo "$JAVA_HOME" |
|
28 |
echo "$(platform_path "$ISABELLE_CLASSPATH")" |
|
29 |
for ARG in "${JAVA_ARGS[@]}"; do echo "$ARG"; done |
|
30 |
) | { |
|
31 |
LINE_COUNT=0 |
|
32 |
export ISABELLE_ROOT="" |
|
33 |
export CYGWIN_ROOT="" |
|
34 |
unset JAVA_HOME |
|
35 |
unset ISABELLE_CLASSPATH |
|
36 |
unset JAVA_ARGS; declare -a JAVA_ARGS |
|
37 |
||
38 |
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } |
|
39 |
do |
|
40 |
case "$LINE_COUNT" in |
|
41 |
0) |
|
42 |
LINE_COUNT=1 |
|
43 |
ISABELLE_ROOT="$REPLY" |
|
44 |
;; |
|
45 |
1) |
|
46 |
LINE_COUNT=2 |
|
47 |
CYGWIN_ROOT="$REPLY" |
|
48 |
;; |
|
49 |
2) |
|
50 |
LINE_COUNT=3 |
|
51 |
JAVA_HOME="$REPLY" |
|
52 |
;; |
|
53 |
3) |
|
54 |
LINE_COUNT=4 |
|
55 |
ISABELLE_CLASSPATH="$REPLY" |
|
56 |
;; |
|
57 |
*) |
|
58 |
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$REPLY" |
|
59 |
;; |
|
60 |
esac |
|
61 |
done |
|
62 |
||
63 |
if [ -z "$JAVA_HOME" ]; then |
|
64 |
echo "Unknown JAVA_HOME -- Java unavailable" >&2 |
|
65 |
exit 127 |
|
66 |
else |
|
64022 | 67 |
unset ISABELLE_HOME |
63995 | 68 |
unset CLASSPATH |
67490
982f0bf34804
more robust java.ext.dirs: avoid picking up accidental jars from system directories;
wenzelm
parents:
66906
diff
changeset
|
69 |
exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \ |
982f0bf34804
more robust java.ext.dirs: avoid picking up accidental jars from system directories;
wenzelm
parents:
66906
diff
changeset
|
70 |
-classpath "$ISABELLE_CLASSPATH" "$@" |
63995 | 71 |
fi |
72 |
} |