lib/scripts/getsettings

tuned message, which is displayed after termination of Isabelle.app on Mac OS;

+
−# -*- shell-script -*- :mode=shellscript:
+
−#
+
−# 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!"
+
−  echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
+
−fi
+
−
+
−#key executables
+
−ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
+
−ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
+
−
+
−function isabelle ()
+
−{
+
−  "$ISABELLE_TOOL" "$@"
+
−}
+
−
+
−#platform
+
−source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
+
−
+
−#Isabelle distribution identifier -- filled in automatically!
+
−ISABELLE_ID=""
+
−ISABELLE_IDENTIFIER=""
+
−
+
−#sometimes users 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 wrapper
+
−if [ "$OSTYPE" = cygwin ]; then
+
−  CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
+
−  function jvmpath() { cygpath -C UTF8 -w -p "$@"; }
+
−  THIS_CYGWIN="$(jvmpath "/")"
+
−else
+
−  function jvmpath() { echo "$@"; }
+
−  CLASSPATH="$CLASSPATH"
+
−fi
+
−HOME_JVM="$HOME"
+
−
+
−#shared library convenience
+
−function librarypath () {
+
−  for X in "$@"
+
−  do
+
−    case "$ISABELLE_PLATFORM" in
+
−      *-darwin)
+
−        if [ -z "$DYLD_LIBRARY_PATH" ]; then
+
−          DYLD_LIBRARY_PATH="$X"
+
−        else
+
−          DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
+
−        fi
+
−        export DYLD_LIBRARY_PATH
+
−        ;;
+
−      *)
+
−        if [ -z "$LD_LIBRARY_PATH" ]; then
+
−          LD_LIBRARY_PATH="$X"
+
−        else
+
−          LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
+
−        fi
+
−        export LD_LIBRARY_PATH
+
−        ;;
+
−    esac
+
−  done
+
−}
+
−
+
−#CLASSPATH convenience
+
−function classpath () {
+
−  for X in "$@"
+
−  do
+
−    if [ -z "$CLASSPATH" ]; then
+
−      CLASSPATH="$X"
+
−    else
+
−      CLASSPATH="$X:$CLASSPATH"
+
−    fi
+
−  done
+
−  export CLASSPATH
+
−}
+
−
+
−#arrays
+
−function splitarray ()
+
−{
+
−  SPLITARRAY=()
+
−  local IFS="$1"; shift
+
−  for X in $*
+
−  do
+
−    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
+
−  done
+
−}
+
−
+
−#nested components
+
−ISABELLE_COMPONENTS=""
+
−function init_component ()
+
−{
+
−  local COMPONENT="$1"
+
−  case "$COMPONENT" in
+
−    /*) ;;
+
−    *)
+
−      echo >&2 "Absolute component path required: \"$COMPONENT\""
+
−      exit 2
+
−      ;;
+
−  esac
+
−
+
−  if [ ! -d "$COMPONENT" ]; then
+
−    echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
+
−    exit 2
+
−  elif [ -z "$ISABELLE_COMPONENTS" ]; then
+
−    ISABELLE_COMPONENTS="$COMPONENT"
+
−  else
+
−    ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+
−  fi
+
−  if [ -f "$COMPONENT/etc/settings" ]; then
+
−    source "$COMPONENT/etc/settings"
+
−    local RC="$?"
+
−    if [ "$RC" -ne 0 ]; then
+
−      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
+
−      exit 2
+
−    fi
+
−  fi
+
−  if [ -f "$COMPONENT/etc/components" ]; then
+
−    {
+
−      while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+
−      do
+
−        case "$REPLY" in
+
−          \#* | "") ;;
+
−          /*) init_component "$REPLY" ;;
+
−          *) init_component "$COMPONENT/$REPLY" ;;
+
−        esac
+
−      done
+
−    } < "$COMPONENT/etc/components"
+
−  fi
+
−}
+
−
+
−#main components
+
−init_component "$ISABELLE_HOME"
+
−[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
+
−
+
−#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