lib/scripts/getsettings
author wenzelm
Sat Sep 28 13:50:38 2013 +0200 (2013-09-28)
changeset 53967 bfaae48b0ce0
parent 53913 5ff12177a067
child 53970 eee1863c565a
permissions -rwxr-xr-x
simplified ISABELLE_HOME on Windows (see also 9c8a1b9c0630, 5a7903ba2dac);
     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 #GNU tar (notably on Mac OS X)
    15 if [ -x /usr/bin/gnutar ]; then
    16   function tar() { /usr/bin/gnutar "$@"; }
    17 fi
    18 
    19 #Cygwin vs. POSIX
    20 if [ "$OSTYPE" = cygwin ]
    21 then
    22   if [ -z "$USER_HOME" ]; then
    23     USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
    24   fi
    25 
    26   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    27   CYGWIN_ROOT="$(jvmpath "/")"
    28 
    29   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    30   unset CLASSPATH
    31 else
    32   if [ -z "$USER_HOME" ]; then
    33     USER_HOME="$HOME"
    34   fi
    35 
    36   function jvmpath() { echo "$@"; }
    37 
    38   ISABELLE_CLASSPATH="$CLASSPATH"
    39   unset CLASSPATH
    40 fi
    41 
    42 export ISABELLE_HOME
    43 
    44 #key executables
    45 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    46 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    47 
    48 function isabelle ()
    49 {
    50   "$ISABELLE_TOOL" "$@"
    51 }
    52 
    53 #platform
    54 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    55 if [ -z "$ISABELLE_PLATFORM" ]; then
    56   echo 1>&2 "Failed to determine hardware and operating system type!"
    57   exit 2
    58 fi
    59 
    60 #Isabelle distribution identifier -- filled in automatically!
    61 ISABELLE_ID=""
    62 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    63 
    64 #sometimes users put strange things in here ...
    65 unset ENV
    66 unset BASH_ENV
    67 
    68 #shared library convenience
    69 function librarypath ()
    70 {
    71   for X in "$@"
    72   do
    73     case "$ISABELLE_PLATFORM" in
    74       *-darwin)
    75         if [ -z "$DYLD_LIBRARY_PATH" ]; then
    76           DYLD_LIBRARY_PATH="$X"
    77         else
    78           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    79         fi
    80         export DYLD_LIBRARY_PATH
    81         ;;
    82       *)
    83         if [ -z "$LD_LIBRARY_PATH" ]; then
    84           LD_LIBRARY_PATH="$X"
    85         else
    86           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
    87         fi
    88         export LD_LIBRARY_PATH
    89         ;;
    90     esac
    91   done
    92 }
    93 
    94 #robust invocation via ISABELLE_JDK_HOME
    95 function isabelle_jdk ()
    96 {
    97   if [ -z "$ISABELLE_JDK_HOME" ]; then
    98     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
    99     return 127
   100   else
   101     local PRG="$1"; shift
   102     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   103   fi
   104 }
   105 
   106 #robust invocation via SCALA_HOME
   107 function isabelle_scala ()
   108 {
   109   if [ -z "$ISABELLE_JDK_HOME" ]; then
   110     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
   111     return 127
   112   elif [ -z "$SCALA_HOME" ]; then
   113     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   114     return 127
   115   else
   116     local PRG="$1"; shift
   117     "$SCALA_HOME/bin/$PRG" "$@"
   118   fi
   119 }
   120 
   121 #administrative build
   122 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   123   function isabelle_admin_build ()
   124   {
   125     "$ISABELLE_HOME/Admin/build" "$@"
   126   }
   127 else
   128   function isabelle_admin_build () { return 0; }
   129 fi
   130 
   131 #classpath
   132 function classpath ()
   133 {
   134   for X in "$@"
   135   do
   136     if [ -z "$ISABELLE_CLASSPATH" ]; then
   137       ISABELLE_CLASSPATH="$X"
   138     else
   139       ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
   140     fi
   141   done
   142   export ISABELLE_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 
   157 # components
   158 
   159 ISABELLE_COMPONENTS=""
   160 ISABELLE_COMPONENTS_MISSING=""
   161 
   162 #init component tree
   163 function init_component ()
   164 {
   165   local COMPONENT="$1"
   166   case "$COMPONENT" in
   167     /*) ;;
   168     *)
   169       echo >&2 "Absolute component path required: \"$COMPONENT\""
   170       exit 2
   171       ;;
   172   esac
   173 
   174   if [ -d "$COMPONENT" ]; then
   175     if [ -z "$ISABELLE_COMPONENTS" ]; then
   176       ISABELLE_COMPONENTS="$COMPONENT"
   177     else
   178       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   179     fi
   180   else
   181     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   182     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   183       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   184     else
   185       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   186     fi
   187   fi
   188 
   189   if [ -f "$COMPONENT/etc/settings" ]; then
   190     source "$COMPONENT/etc/settings"
   191     local RC="$?"
   192     if [ "$RC" -ne 0 ]; then
   193       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   194       exit 2
   195     fi
   196   fi
   197   if [ -f "$COMPONENT/etc/components" ]; then
   198     init_components "$COMPONENT" "$COMPONENT/etc/components"
   199   fi
   200 }
   201 
   202 #init component forest
   203 function init_components ()
   204 {
   205   local BASE="$1"
   206   local CATALOG="$2"
   207 
   208   if [ ! -f "$CATALOG" ]; then
   209     echo >&2 "Bad component catalog file: \"$CATALOG\""
   210     exit 2
   211   fi
   212   {
   213     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   214     do
   215       case "$REPLY" in
   216         \#* | "") ;;
   217         /*) init_component "$REPLY" ;;
   218         *) init_component "$BASE/$REPLY" ;;
   219       esac
   220     done
   221   } < "$CATALOG"
   222 }
   223 
   224 #main components
   225 init_component "$ISABELLE_HOME"
   226 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   227 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   228 
   229 
   230 #ML system identifier
   231 if [ -z "$ML_PLATFORM" ]; then
   232   ML_IDENTIFIER="$ML_SYSTEM"
   233 else
   234   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   235 fi
   236 
   237 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   238 
   239 #enforce JAVA_HOME
   240 export JAVA_HOME="$ISABELLE_JDK_HOME"
   241 
   242 #build condition etc.
   243 case "$ML_SYSTEM" in
   244   polyml*)
   245     ISABELLE_POLYML="true"
   246     ;;
   247   *)
   248     ISABELLE_POLYML=""
   249     ;;
   250 esac
   251 
   252 set +o allexport
   253 
   254 fi