# -*- shell-script -*- # $Id: getsettings,v 1.24 2005/06/06 07:28:28 kleing Exp $ # Author: Markus Wenzel, TU Muenchen # # getsettings - sh 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" #users tend to put strange things in here ... unset ENV #support easy settings choosefrom () { local RESULT="" local FILE="" for FILE in "$@" do [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE" done [ -z "$RESULT" ] && RESULT="$FILE" echo "$RESULT" } #get actual settings . "$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" ] && \ { . "$ISABELLE_HOME_USER/etc/settings" || exit 2; } #append ML system identifier to paths 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