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