lib/scripts/getsettings
author wenzelm
Fri Aug 17 11:42:05 2012 +0200 (2012-08-17)
changeset 48837 d1d806a42c91
parent 48790 6e739225dd8a
child 48838 623ba165d059
permissions -rwxr-xr-x
allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira;
clarified spaces in file names -- ISABELLE_HOME is non-critical after abolishment of "make";
     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 #nested components
   152 ISABELLE_COMPONENTS=""
   153 function init_component ()
   154 {
   155   local COMPONENT="$1"
   156   case "$COMPONENT" in
   157     /*) ;;
   158     *)
   159       echo >&2 "Absolute component path required: \"$COMPONENT\""
   160       exit 2
   161       ;;
   162   esac
   163 
   164   if [ ! -d "$COMPONENT" ]; then
   165     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   166   elif [ -z "$ISABELLE_COMPONENTS" ]; then
   167     ISABELLE_COMPONENTS="$COMPONENT"
   168   else
   169     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   170   fi
   171   if [ -f "$COMPONENT/etc/settings" ]; then
   172     source "$COMPONENT/etc/settings"
   173     local RC="$?"
   174     if [ "$RC" -ne 0 ]; then
   175       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   176       exit 2
   177     fi
   178   fi
   179   if [ -f "$COMPONENT/etc/components" ]; then
   180     {
   181       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   182       do
   183         case "$REPLY" in
   184           \#* | "") ;;
   185           /*) init_component "$REPLY" ;;
   186           *) init_component "$COMPONENT/$REPLY" ;;
   187         esac
   188       done
   189     } < "$COMPONENT/etc/components"
   190   fi
   191 }
   192 
   193 #main components
   194 init_component "$ISABELLE_HOME"
   195 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   196 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   197 
   198 #ML system identifier
   199 if [ -z "$ML_PLATFORM" ]; then
   200   ML_IDENTIFIER="$ML_SYSTEM"
   201 else
   202   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   203 fi
   204 
   205 #enforce JAVA_HOME
   206 export JAVA_HOME="$ISABELLE_JDK_HOME"
   207 
   208 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   209 
   210 #build condition etc.
   211 case "$ML_SYSTEM" in
   212   polyml*)
   213     ISABELLE_POLYML="true"
   214     ;;
   215   *)
   216     ISABELLE_POLYML=""
   217     ;;
   218 esac
   219 
   220 set +o allexport
   221 
   222 fi