lib/scripts/getsettings
author wenzelm
Wed Apr 25 15:13:03 2012 +0200 (2012-04-25)
changeset 47748 24550210de0b
parent 47661 012a887997f3
child 47996 25b9f59ab1b9
permissions -rwxr-xr-x
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
     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 #Cygwin vs Posix
    15 if [ "$OSTYPE" = cygwin ]
    16 then
    17   if [ -z "$USER_HOME" ]; then
    18     USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
    19   fi
    20 
    21   ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
    22   ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
    23 
    24   CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    25   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    26   THIS_CYGWIN="$(jvmpath "/")"
    27 else
    28   if [ -z "$USER_HOME" ]; then
    29     USER_HOME="$HOME"
    30   fi
    31 
    32   function jvmpath() { echo "$@"; }
    33   CLASSPATH="$CLASSPATH"
    34 fi
    35 
    36 export ISABELLE_HOME
    37 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
    38 then
    39   echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
    40   echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    41 fi
    42 
    43 #key executables
    44 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    45 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    46 
    47 function isabelle ()
    48 {
    49   "$ISABELLE_TOOL" "$@"
    50 }
    51 
    52 #platform
    53 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    54 
    55 #Isabelle distribution identifier -- filled in automatically!
    56 ISABELLE_ID=""
    57 ISABELLE_IDENTIFIER=""
    58 
    59 #sometimes users put strange things in here ...
    60 unset ENV
    61 unset BASH_ENV
    62 
    63 #support easy settings
    64 function choosefrom ()
    65 {
    66   local RESULT=""
    67   local FILE=""
    68 
    69   for FILE in "$@"
    70   do
    71     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    72   done
    73 
    74   [ -z "$RESULT" ] && RESULT="$FILE"
    75   echo "$RESULT"
    76 }
    77 
    78 #shared library convenience
    79 function librarypath () {
    80   for X in "$@"
    81   do
    82     case "$ISABELLE_PLATFORM" in
    83       *-darwin)
    84         if [ -z "$DYLD_LIBRARY_PATH" ]; then
    85           DYLD_LIBRARY_PATH="$X"
    86         else
    87           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    88         fi
    89         export DYLD_LIBRARY_PATH
    90         ;;
    91       *)
    92         if [ -z "$LD_LIBRARY_PATH" ]; then
    93           LD_LIBRARY_PATH="$X"
    94         else
    95           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
    96         fi
    97         export LD_LIBRARY_PATH
    98         ;;
    99     esac
   100   done
   101 }
   102 
   103 #robust invocation via ISABELLE_JDK_HOME
   104 function isabelle_jdk () {
   105   if [ -z "$ISABELLE_JDK_HOME" ]; then
   106     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   107     return 127
   108   else
   109     local PRG="$1"; shift
   110     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   111   fi
   112 }
   113 
   114 #robust invocation via SCALA_HOME
   115 function isabelle_scala () {
   116   if [ -z "$ISABELLE_JDK_HOME" ]; then
   117     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   118     return 127
   119   elif [ -z "$SCALA_HOME" ]; then
   120     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   121     return 127
   122   else
   123     local PRG="$1"; shift
   124     "$SCALA_HOME/bin/$PRG" "$@"
   125   fi
   126 }
   127 
   128 #CLASSPATH convenience
   129 function classpath () {
   130   for X in "$@"
   131   do
   132     if [ -z "$CLASSPATH" ]; then
   133       CLASSPATH="$X"
   134     else
   135       CLASSPATH="$X:$CLASSPATH"
   136     fi
   137   done
   138   export CLASSPATH
   139 }
   140 
   141 #arrays
   142 function splitarray ()
   143 {
   144   SPLITARRAY=()
   145   local IFS="$1"; shift
   146   for X in $*
   147   do
   148     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   149   done
   150 }
   151 
   152 #nested components
   153 ISABELLE_COMPONENTS=""
   154 function init_component ()
   155 {
   156   local COMPONENT="$1"
   157   case "$COMPONENT" in
   158     /*) ;;
   159     *)
   160       echo >&2 "Absolute component path required: \"$COMPONENT\""
   161       exit 2
   162       ;;
   163   esac
   164 
   165   if [ ! -d "$COMPONENT" ]; then
   166     echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
   167     exit 2
   168   elif [ -z "$ISABELLE_COMPONENTS" ]; then
   169     ISABELLE_COMPONENTS="$COMPONENT"
   170   else
   171     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   172   fi
   173   if [ -f "$COMPONENT/etc/settings" ]; then
   174     source "$COMPONENT/etc/settings"
   175     local RC="$?"
   176     if [ "$RC" -ne 0 ]; then
   177       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   178       exit 2
   179     fi
   180   fi
   181   if [ -f "$COMPONENT/etc/components" ]; then
   182     {
   183       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   184       do
   185         case "$REPLY" in
   186           \#* | "") ;;
   187           /*) init_component "$REPLY" ;;
   188           *) init_component "$COMPONENT/$REPLY" ;;
   189         esac
   190       done
   191     } < "$COMPONENT/etc/components"
   192   fi
   193 }
   194 
   195 #main components
   196 init_component "$ISABELLE_HOME"
   197 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   198 
   199 #ML system identifier
   200 if [ -z "$ML_PLATFORM" ]; then
   201   ML_IDENTIFIER="$ML_SYSTEM"
   202 else
   203   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   204 fi
   205 
   206 #enforce JAVA_HOME
   207 export JAVA_HOME="$ISABELLE_JDK_HOME"
   208 
   209 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   210 
   211 set +o allexport
   212 
   213 fi