lib/scripts/getsettings
author wenzelm
Sat Oct 04 17:40:56 2008 +0200 (2008-10-04)
changeset 28504 7ad7d7d6df47
parent 28499 eff93bc3c14f
child 29145 b1c6f4563df7
permissions -rw-r--r--
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
     1 # -*- shell-script -*- :mode=shellscript:
     2 # $Id$
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # getsettings - bash source script to augment current env.
     6 
     7 if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
     8 then
     9 
    10 set -o allexport
    11 
    12 ISABELLE_SETTINGS_PRESENT=true
    13 
    14 export ISABELLE_HOME
    15 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
    16 then
    17   echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
    18   echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    19 fi
    20 
    21 #key executables
    22 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    23 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    24 #legacy settings
    25 ISABELLE="$ISABELLE_PROCESS"
    26 ISATOOL="$ISABELLE_TOOL"
    27 
    28 #Isabelle distribution identifier -- filled in automatically!
    29 ISABELLE_IDENTIFIER=""
    30 
    31 #users tend to put strange things in here ...
    32 unset ENV
    33 unset BASH_ENV
    34 
    35 #support easy settings
    36 function choosefrom ()
    37 {
    38   local RESULT=""
    39   local FILE=""
    40 
    41   for FILE in "$@"
    42   do
    43     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    44   done
    45 
    46   [ -z "$RESULT" ] && RESULT="$FILE"
    47   echo "$RESULT"
    48 }
    49 
    50 #JVM path wrapper
    51 if [ "$OSTYPE" = cygwin ]; then
    52   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
    53   function jvmpath() { cygpath -w -p "$@"; }
    54   ISABELLE_ROOT_JVM="$(jvmpath /)"
    55 else
    56   function jvmpath() { echo "$@"; }
    57   ISABELLE_ROOT_JVM=/
    58 fi
    59 HOME_JVM="$HOME"
    60 
    61 #CLASSPATH convenience
    62 function classpath () {
    63   for X in "$@"
    64   do
    65     if [ -z "$CLASSPATH" ]; then
    66       CLASSPATH="$X"
    67     else
    68       CLASSPATH="$CLASSPATH:$X"
    69     fi
    70   done
    71 }
    72 
    73 #get actual settings
    74 source "$ISABELLE_HOME/etc/settings" || exit 2
    75 ISABELLE_SITE_SETTINGS_PRESENT=true
    76 
    77 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
    78   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
    79 [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
    80   { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
    81 
    82 #ML system identifier
    83 if [ -z "$ML_PLATFORM" ]; then
    84   ML_IDENTIFIER="$ML_SYSTEM"
    85 else
    86   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
    87 fi
    88 
    89 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
    90 
    91 set +o allexport
    92 
    93 fi