| author | immler | 
| Mon, 07 Jan 2019 13:16:33 +0100 | |
| changeset 69617 | 63ee37c519a3 | 
| 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: 
66906diff
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: 
66906diff
changeset | 70 | -classpath "$ISABELLE_CLASSPATH" "$@" | 
| 63995 | 71 | fi | 
| 72 | } |