lib/scripts/getsettings
author wenzelm
Wed Jan 19 21:00:16 2011 +0100 (2011-01-19)
changeset 41614 b7cd80330a16
parent 41511 2fe62d602681
child 41615 f70d2cb26acf
permissions -rw-r--r--
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
     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 
    25 function isabelle ()
    26 {
    27   "$ISABELLE_TOOL" "$@"
    28 }
    29 
    30 #platform
    31 . "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    32 
    33 #Isabelle distribution identifier -- filled in automatically!
    34 ISABELLE_ID=""
    35 ISABELLE_IDENTIFIER=""
    36 
    37 #sometimes users put strange things in here ...
    38 unset ENV
    39 unset BASH_ENV
    40 
    41 #support easy settings
    42 function choosefrom ()
    43 {
    44   local RESULT=""
    45   local FILE=""
    46 
    47   for FILE in "$@"
    48   do
    49     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    50   done
    51 
    52   [ -z "$RESULT" ] && RESULT="$FILE"
    53   echo "$RESULT"
    54 }
    55 
    56 #JVM path wrapper
    57 if [ "$OSTYPE" = cygwin ]; then
    58   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
    59   function jvmpath() { cygpath -w -p "$@"; }
    60   THIS_CYGWIN="$(jvmpath "/")"
    61 else
    62   function jvmpath() { echo "$@"; }
    63 fi
    64 HOME_JVM="$HOME"
    65 
    66 #shared library convenience
    67 function librarypath () {
    68   for X in "$@"
    69   do
    70     case "$ISABELLE_PLATFORM" in
    71       *-darwin)
    72         if [ -z "$DYLD_LIBRARY_PATH" ]; then
    73           DYLD_LIBRARY_PATH="$X"
    74         else
    75           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    76         fi
    77         export DYLD_LIBRARY_PATH
    78         ;;
    79       *)
    80         if [ -z "$LD_LIBRARY_PATH" ]; then
    81           LD_LIBRARY_PATH="$X"
    82         else
    83           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
    84         fi
    85         export LD_LIBRARY_PATH
    86         ;;
    87     esac
    88   done
    89 }
    90 
    91 #CLASSPATH convenience
    92 function classpath () {
    93   for X in "$@"
    94   do
    95     if [ -z "$CLASSPATH" ]; then
    96       CLASSPATH="$X"
    97     else
    98       CLASSPATH="$CLASSPATH:$X"
    99     fi
   100   done
   101   export CLASSPATH
   102 }
   103 
   104 #arrays
   105 function splitarray ()
   106 {
   107   SPLITARRAY=()
   108   local IFS="$1"; shift
   109   for X in $*
   110   do
   111     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   112   done
   113 }
   114 
   115 #nested components
   116 ISABELLE_COMPONENTS=""
   117 function init_component ()
   118 {
   119   local COMPONENT="$1"
   120   case "$COMPONENT" in
   121     /*) ;;
   122     *)
   123       echo >&2 "Absolute component path required: \"$COMPONENT\""
   124       exit 2
   125       ;;
   126   esac
   127 
   128   if [ ! -d "$COMPONENT" ]; then
   129     echo >&2 "Bad Isabelle component: \"$COMPONENT\""
   130     exit 2
   131   elif [ -z "$ISABELLE_COMPONENTS" ]; then
   132     ISABELLE_COMPONENTS="$COMPONENT"
   133   else
   134     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   135   fi
   136   if [ -f "$COMPONENT/etc/settings" ]; then
   137     source "$COMPONENT/etc/settings" || exit 2
   138   fi
   139   if [ -f "$COMPONENT/etc/components" ]; then
   140     {
   141       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   142       do
   143         case "$REPLY" in
   144           \#* | "") ;;
   145           /*) init_component "$REPLY" ;;
   146           *) init_component "$COMPONENT/$REPLY" ;;
   147         esac
   148       done
   149     } < "$COMPONENT/etc/components"
   150   fi
   151 }
   152 
   153 #main components
   154 init_component "$ISABELLE_HOME"
   155 
   156 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
   157   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
   158 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   159 
   160 #ML system identifier
   161 if [ -z "$ML_PLATFORM" ]; then
   162   ML_IDENTIFIER="$ML_SYSTEM"
   163 else
   164   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   165 fi
   166 
   167 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   168 
   169 set +o allexport
   170 
   171 fi