lib/scripts/getsettings
author wenzelm
Wed Oct 28 22:57:32 2009 +0100 (2009-10-28)
changeset 33294 e2a11715aab1
parent 33286 1807921b6268
child 33295 ce8faf41b0d4
permissions -rw-r--r--
components: ensure that the last line is read, even if it lacks EOL;
     1 # -*- shell-script -*- :mode=shellscript:
     2 #
     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 unset POSIXLY_CORRECT
    35 set +o posix
    36 
    37 #support easy settings
    38 function choosefrom ()
    39 {
    40   local RESULT=""
    41   local FILE=""
    42 
    43   for FILE in "$@"
    44   do
    45     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    46   done
    47 
    48   [ -z "$RESULT" ] && RESULT="$FILE"
    49   echo "$RESULT"
    50 }
    51 
    52 #JVM path wrapper
    53 if [ "$OSTYPE" = cygwin ]; then
    54   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
    55   function jvmpath() { cygpath -w -p "$@"; }
    56 else
    57   function jvmpath() { echo "$@"; }
    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 #arrays
    74 function splitarray ()
    75 {
    76   SPLITARRAY=()
    77   local IFS="$1"; shift
    78   for X in $*
    79   do
    80     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
    81   done
    82 }
    83 
    84 #nested components
    85 ISABELLE_COMPONENTS=""
    86 function init_component ()
    87 {
    88   local COMPONENT="$1"
    89 
    90   if [ ! -d "$COMPONENT" ]; then
    91     echo >&2 "Bad Isabelle component: \"$COMPONENT"\"
    92     exit 2
    93   elif [ -z "$ISABELLE_COMPONENTS" ]; then
    94     ISABELLE_COMPONENTS="$COMPONENT"
    95   else
    96     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    97   fi
    98   if [ -f "$COMPONENT/etc/settings" ]; then
    99     source "$COMPONENT/etc/settings" || exit 2
   100   fi
   101   if [ -f "$COMPONENT/etc/components" ]; then
   102     {
   103       while read; do
   104         case "$REPLY" in
   105           \#* | "") ;;
   106           /*) init_component "$REPLY" ;;
   107           *) init_component "$COMPONENT/$REPLY" ;;
   108         esac
   109       done
   110     } < <( cat "$COMPONENT/etc/components"; echo; )
   111   fi
   112 }
   113 
   114 #main components
   115 init_component "$ISABELLE_HOME"
   116 
   117 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
   118   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
   119 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   120 
   121 #ML system identifier
   122 if [ -z "$ML_PLATFORM" ]; then
   123   ML_IDENTIFIER="$ML_SYSTEM"
   124 else
   125   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   126 fi
   127 
   128 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   129 
   130 set +o allexport
   131 
   132 fi