lib/scripts/getsettings
author wenzelm
Fri Aug 17 12:14:58 2012 +0200 (2012-08-17)
changeset 48838 623ba165d059
parent 48837 d1d806a42c91
child 49000 0cebcbeac4c7
permissions -rwxr-xr-x
direct support for component forests via init_components;
explicit ISABELLE_COMPONENTS_MISSING;
     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   CYGWIN_ROOT="$(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 
    38 #key executables
    39 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    40 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    41 
    42 function isabelle ()
    43 {
    44   "$ISABELLE_TOOL" "$@"
    45 }
    46 
    47 #platform
    48 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    49 if [ -z "$ISABELLE_PLATFORM" ]; then
    50   echo 1>&2 "Failed to determine hardware and operating system type!"
    51   exit 2
    52 fi
    53 
    54 #Isabelle distribution identifier -- filled in automatically!
    55 ISABELLE_ID=""
    56 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    57 
    58 #sometimes users put strange things in here ...
    59 unset ENV
    60 unset BASH_ENV
    61 
    62 #support easy settings
    63 function choosefrom ()
    64 {
    65   local RESULT=""
    66   local FILE=""
    67 
    68   for FILE in "$@"
    69   do
    70     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    71   done
    72 
    73   [ -z "$RESULT" ] && RESULT="$FILE"
    74   echo "$RESULT"
    75 }
    76 
    77 #shared library convenience
    78 function librarypath () {
    79   for X in "$@"
    80   do
    81     case "$ISABELLE_PLATFORM" in
    82       *-darwin)
    83         if [ -z "$DYLD_LIBRARY_PATH" ]; then
    84           DYLD_LIBRARY_PATH="$X"
    85         else
    86           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    87         fi
    88         export DYLD_LIBRARY_PATH
    89         ;;
    90       *)
    91         if [ -z "$LD_LIBRARY_PATH" ]; then
    92           LD_LIBRARY_PATH="$X"
    93         else
    94           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
    95         fi
    96         export LD_LIBRARY_PATH
    97         ;;
    98     esac
    99   done
   100 }
   101 
   102 #robust invocation via ISABELLE_JDK_HOME
   103 function isabelle_jdk () {
   104   if [ -z "$ISABELLE_JDK_HOME" ]; then
   105     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   106     return 127
   107   else
   108     local PRG="$1"; shift
   109     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   110   fi
   111 }
   112 
   113 #robust invocation via SCALA_HOME
   114 function isabelle_scala () {
   115   if [ -z "$ISABELLE_JDK_HOME" ]; then
   116     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   117     return 127
   118   elif [ -z "$SCALA_HOME" ]; then
   119     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   120     return 127
   121   else
   122     local PRG="$1"; shift
   123     "$SCALA_HOME/bin/$PRG" "$@"
   124   fi
   125 }
   126 
   127 #CLASSPATH convenience
   128 function classpath () {
   129   for X in "$@"
   130   do
   131     if [ -z "$CLASSPATH" ]; then
   132       CLASSPATH="$X"
   133     else
   134       CLASSPATH="$X:$CLASSPATH"
   135     fi
   136   done
   137   export CLASSPATH
   138 }
   139 
   140 #arrays
   141 function splitarray ()
   142 {
   143   SPLITARRAY=()
   144   local IFS="$1"; shift
   145   for X in $*
   146   do
   147     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   148   done
   149 }
   150 
   151 
   152 # components
   153 
   154 ISABELLE_COMPONENTS=""
   155 ISABELLE_COMPONENTS_MISSING=""
   156 
   157 #init component tree
   158 function init_component ()
   159 {
   160   local COMPONENT="$1"
   161   case "$COMPONENT" in
   162     /*) ;;
   163     *)
   164       echo >&2 "Absolute component path required: \"$COMPONENT\""
   165       exit 2
   166       ;;
   167   esac
   168 
   169   if [ -d "$COMPONENT" ]; then
   170     if [ -z "$ISABELLE_COMPONENTS" ]; then
   171       ISABELLE_COMPONENTS="$COMPONENT"
   172     else
   173       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   174     fi
   175   else
   176     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   177     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   178       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   179     else
   180       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   181     fi
   182   fi
   183 
   184   if [ -f "$COMPONENT/etc/settings" ]; then
   185     source "$COMPONENT/etc/settings"
   186     local RC="$?"
   187     if [ "$RC" -ne 0 ]; then
   188       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   189       exit 2
   190     fi
   191   fi
   192   if [ -f "$COMPONENT/etc/components" ]; then
   193     init_components "$COMPONENT" "$COMPONENT/etc/components"
   194   fi
   195 }
   196 
   197 #init component forest
   198 function init_components ()
   199 {
   200   local BASE="$1"
   201   local CATALOG="$2"
   202 
   203   if [ ! -d "$BASE" ]; then
   204     echo >&2 "Bad component base directory: \"$BASE\""
   205     exit 2
   206   fi
   207   if [ ! -f "$CATALOG" ]; then
   208     echo >&2 "Bad component catalog file: \"$CATALOG\""
   209     exit 2
   210   fi
   211   {
   212     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   213     do
   214       case "$REPLY" in
   215         \#* | "") ;;
   216         /*) init_component "$REPLY" ;;
   217         *) init_component "$BASE/$REPLY" ;;
   218       esac
   219     done
   220   } < "$CATALOG"
   221 }
   222 
   223 #main components
   224 init_component "$ISABELLE_HOME"
   225 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   226 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   227 
   228 
   229 #ML system identifier
   230 if [ -z "$ML_PLATFORM" ]; then
   231   ML_IDENTIFIER="$ML_SYSTEM"
   232 else
   233   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   234 fi
   235 
   236 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   237 
   238 #enforce JAVA_HOME
   239 export JAVA_HOME="$ISABELLE_JDK_HOME"
   240 
   241 #build condition etc.
   242 case "$ML_SYSTEM" in
   243   polyml*)
   244     ISABELLE_POLYML="true"
   245     ;;
   246   *)
   247     ISABELLE_POLYML=""
   248     ;;
   249 esac
   250 
   251 set +o allexport
   252 
   253 fi