lib/scripts/getsettings

added ISABELLE_HOME_JVM;

+
−# -*- shell-script -*- :mode=shellscript:
+
−# $Id$
+
−# Author: Markus Wenzel, TU Muenchen
+
−#
+
−# getsettings - bash source script to augment current env.
+
−
+
−if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
+
−then
+
−
+
−set -o allexport
+
−
+
−ISABELLE_SETTINGS_PRESENT=true
+
−
+
−export ISABELLE_HOME
+
−if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
+
−then
+
−  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
+
−  echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
+
−fi
+
−
+
−#key executables
+
−ISABELLE="$ISABELLE_HOME/bin/isabelle-process"
+
−ISATOOL="$ISABELLE_HOME/bin/isatool"
+
−
+
−#Isabelle distribution identifier -- filled in automatically!
+
−ISABELLE_IDENTIFIER=""
+
−
+
−#users tend to put strange things in here ...
+
−unset ENV
+
−unset BASH_ENV
+
−
+
−#support easy settings
+
−function choosefrom ()
+
−{
+
−  local RESULT=""
+
−  local FILE=""
+
−
+
−  for FILE in "$@"
+
−  do
+
−    [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
+
−  done
+
−
+
−  [ -z "$RESULT" ] && RESULT="$FILE"
+
−  echo "$RESULT"
+
−}
+
−
+
−#JVM path wrappers
+
−if [ "$OSTYPE" = cygwin ]; then
+
−  CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
+
−  function jvmpath() { cygpath -w -p "$@"; }
+
−  function javawrapper() { env CLASSPATH="$(jvmpath "$CLASSPATH")" java "$@"; }
+
−  function scalawrapper() { env CLASSPATH="$(jvmpath "$CLASSPATH")" scala "$@"; }
+
−else
+
−  function jvmpath() { echo "$@"; }
+
−  function javawrapper() { java "$@"; }
+
−  function scalawrapper() { scala "$@"; }
+
−fi
+
−ISABELLE_HOME_JVM="$(jvmpath "$ISABELLE_HOME")"
+
−
+
−#CLASSPATH convenience
+
−function classpath () {
+
−  for X in "$@"
+
−  do
+
−    if [ -z "$CLASSPATH" ]; then
+
−      CLASSPATH="$X"
+
−    else
+
−      CLASSPATH="$CLASSPATH:$X"
+
−    fi
+
−  done
+
−}
+
−
+
−#get actual settings
+
−source "$ISABELLE_HOME/etc/settings" || exit 2
+
−ISABELLE_SITE_SETTINGS_PRESENT=true
+
−
+
−[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
+
−  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
+
−[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
+
−  { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
+
−
+
−#ML system identifier
+
−if [ -z "$ML_PLATFORM" ]; then
+
−  ML_IDENTIFIER="$ML_SYSTEM"
+
−else
+
−  ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
+
−fi
+
−
+
−ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
+
−
+
−set +o allexport
+
−
+
−fi