lib/scripts/getsettings
author wenzelm
Tue Aug 14 10:44:03 2012 +0200 (2012-08-14)
changeset 48790 6e739225dd8a
parent 48725 e852f4d6af80
child 48837 d1d806a42c91
permissions -rwxr-xr-x
always retain doc-src (as regular component);
     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 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 if [ -z "$ISABELLE_PLATFORM" ]; then
    55   echo 1>&2 "Failed to determine hardware and operating system type!"
    56   exit 2
    57 fi
    58 
    59 #Isabelle distribution identifier -- filled in automatically!
    60 ISABELLE_ID=""
    61 ISABELLE_IDENTIFIER=""
    62 
    63 #sometimes users put strange things in here ...
    64 unset ENV
    65 unset BASH_ENV
    66 
    67 #support easy settings
    68 function choosefrom ()
    69 {
    70   local RESULT=""
    71   local FILE=""
    72 
    73   for FILE in "$@"
    74   do
    75     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    76   done
    77 
    78   [ -z "$RESULT" ] && RESULT="$FILE"
    79   echo "$RESULT"
    80 }
    81 
    82 #shared library convenience
    83 function librarypath () {
    84   for X in "$@"
    85   do
    86     case "$ISABELLE_PLATFORM" in
    87       *-darwin)
    88         if [ -z "$DYLD_LIBRARY_PATH" ]; then
    89           DYLD_LIBRARY_PATH="$X"
    90         else
    91           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    92         fi
    93         export DYLD_LIBRARY_PATH
    94         ;;
    95       *)
    96         if [ -z "$LD_LIBRARY_PATH" ]; then
    97           LD_LIBRARY_PATH="$X"
    98         else
    99           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
   100         fi
   101         export LD_LIBRARY_PATH
   102         ;;
   103     esac
   104   done
   105 }
   106 
   107 #robust invocation via ISABELLE_JDK_HOME
   108 function isabelle_jdk () {
   109   if [ -z "$ISABELLE_JDK_HOME" ]; then
   110     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   111     return 127
   112   else
   113     local PRG="$1"; shift
   114     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   115   fi
   116 }
   117 
   118 #robust invocation via SCALA_HOME
   119 function isabelle_scala () {
   120   if [ -z "$ISABELLE_JDK_HOME" ]; then
   121     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   122     return 127
   123   elif [ -z "$SCALA_HOME" ]; then
   124     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   125     return 127
   126   else
   127     local PRG="$1"; shift
   128     "$SCALA_HOME/bin/$PRG" "$@"
   129   fi
   130 }
   131 
   132 #CLASSPATH convenience
   133 function classpath () {
   134   for X in "$@"
   135   do
   136     if [ -z "$CLASSPATH" ]; then
   137       CLASSPATH="$X"
   138     else
   139       CLASSPATH="$X:$CLASSPATH"
   140     fi
   141   done
   142   export CLASSPATH
   143 }
   144 
   145 #arrays
   146 function splitarray ()
   147 {
   148   SPLITARRAY=()
   149   local IFS="$1"; shift
   150   for X in $*
   151   do
   152     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   153   done
   154 }
   155 
   156 #nested components
   157 ISABELLE_COMPONENTS=""
   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     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   171   elif [ -z "$ISABELLE_COMPONENTS" ]; then
   172     ISABELLE_COMPONENTS="$COMPONENT"
   173   else
   174     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   175   fi
   176   if [ -f "$COMPONENT/etc/settings" ]; then
   177     source "$COMPONENT/etc/settings"
   178     local RC="$?"
   179     if [ "$RC" -ne 0 ]; then
   180       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   181       exit 2
   182     fi
   183   fi
   184   if [ -f "$COMPONENT/etc/components" ]; then
   185     {
   186       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   187       do
   188         case "$REPLY" in
   189           \#* | "") ;;
   190           /*) init_component "$REPLY" ;;
   191           *) init_component "$COMPONENT/$REPLY" ;;
   192         esac
   193       done
   194     } < "$COMPONENT/etc/components"
   195   fi
   196 }
   197 
   198 #main components
   199 init_component "$ISABELLE_HOME"
   200 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   201 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   202 
   203 #ML system identifier
   204 if [ -z "$ML_PLATFORM" ]; then
   205   ML_IDENTIFIER="$ML_SYSTEM"
   206 else
   207   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   208 fi
   209 
   210 #enforce JAVA_HOME
   211 export JAVA_HOME="$ISABELLE_JDK_HOME"
   212 
   213 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   214 
   215 #build condition etc.
   216 case "$ML_SYSTEM" in
   217   polyml*)
   218     ISABELLE_POLYML="true"
   219     ;;
   220   *)
   221     ISABELLE_POLYML=""
   222     ;;
   223 esac
   224 
   225 set +o allexport
   226 
   227 fi