lib/scripts/getsettings
author wenzelm
Sun Apr 06 16:59:41 2014 +0200 (2014-04-06)
changeset 56439 95e2656b3b23
parent 53970 eee1863c565a
child 56440 aab984137bcd
permissions -rwxr-xr-x
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
     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   unset INI_DIR
    23 
    24   if [ -z "$USER_HOME" ]; then
    25     USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
    26   fi
    27 
    28   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    29   CYGWIN_ROOT="$(jvmpath "/")"
    30 
    31   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    32   unset CLASSPATH
    33 else
    34   if [ -z "$USER_HOME" ]; then
    35     USER_HOME="$HOME"
    36   fi
    37 
    38   function jvmpath() { echo "$@"; }
    39 
    40   ISABELLE_CLASSPATH="$CLASSPATH"
    41   unset CLASSPATH
    42 fi
    43 
    44 export ISABELLE_HOME
    45 
    46 #key executables
    47 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
    48 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    49 
    50 function isabelle_process ()
    51 {
    52   "$ISABELLE_PROCESS" "$@"
    53 }
    54 
    55 function isabelle ()
    56 {
    57   "$ISABELLE_TOOL" "$@"
    58 }
    59 
    60 #platform
    61 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    62 if [ -z "$ISABELLE_PLATFORM" ]; then
    63   echo 1>&2 "Failed to determine hardware and operating system type!"
    64   exit 2
    65 fi
    66 
    67 #Isabelle distribution identifier -- filled in automatically!
    68 ISABELLE_ID=""
    69 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    70 
    71 #sometimes users put strange things in here ...
    72 unset ENV
    73 unset BASH_ENV
    74 
    75 #shared library convenience
    76 function librarypath ()
    77 {
    78   for X in "$@"
    79   do
    80     case "$ISABELLE_PLATFORM" in
    81       *-darwin)
    82         if [ -z "$DYLD_LIBRARY_PATH" ]; then
    83           DYLD_LIBRARY_PATH="$X"
    84         else
    85           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    86         fi
    87         export DYLD_LIBRARY_PATH
    88         ;;
    89       *)
    90         if [ -z "$LD_LIBRARY_PATH" ]; then
    91           LD_LIBRARY_PATH="$X"
    92         else
    93           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
    94         fi
    95         export LD_LIBRARY_PATH
    96         ;;
    97     esac
    98   done
    99 }
   100 
   101 #robust invocation via ISABELLE_JDK_HOME
   102 function isabelle_jdk ()
   103 {
   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 {
   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 #administrative build
   129 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   130   function isabelle_admin_build ()
   131   {
   132     "$ISABELLE_HOME/Admin/build" "$@"
   133   }
   134 else
   135   function isabelle_admin_build () { return 0; }
   136 fi
   137 
   138 #classpath
   139 function classpath ()
   140 {
   141   for X in "$@"
   142   do
   143     if [ -z "$ISABELLE_CLASSPATH" ]; then
   144       ISABELLE_CLASSPATH="$X"
   145     else
   146       ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
   147     fi
   148   done
   149   export ISABELLE_CLASSPATH
   150 }
   151 
   152 #arrays
   153 function splitarray ()
   154 {
   155   SPLITARRAY=()
   156   local IFS="$1"; shift
   157   for X in $*
   158   do
   159     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   160   done
   161 }
   162 
   163 
   164 # components
   165 
   166 ISABELLE_COMPONENTS=""
   167 ISABELLE_COMPONENTS_MISSING=""
   168 
   169 #init component tree
   170 function init_component ()
   171 {
   172   local COMPONENT="$1"
   173   case "$COMPONENT" in
   174     /*) ;;
   175     *)
   176       echo >&2 "Absolute component path required: \"$COMPONENT\""
   177       exit 2
   178       ;;
   179   esac
   180 
   181   if [ -d "$COMPONENT" ]; then
   182     if [ -z "$ISABELLE_COMPONENTS" ]; then
   183       ISABELLE_COMPONENTS="$COMPONENT"
   184     else
   185       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   186     fi
   187   else
   188     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   189     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   190       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   191     else
   192       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   193     fi
   194   fi
   195 
   196   if [ -f "$COMPONENT/etc/settings" ]; then
   197     source "$COMPONENT/etc/settings"
   198     local RC="$?"
   199     if [ "$RC" -ne 0 ]; then
   200       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   201       exit 2
   202     fi
   203   fi
   204   if [ -f "$COMPONENT/etc/components" ]; then
   205     init_components "$COMPONENT" "$COMPONENT/etc/components"
   206   fi
   207 }
   208 
   209 #init component forest
   210 function init_components ()
   211 {
   212   local BASE="$1"
   213   local CATALOG="$2"
   214 
   215   if [ ! -f "$CATALOG" ]; then
   216     echo >&2 "Bad component catalog file: \"$CATALOG\""
   217     exit 2
   218   fi
   219   {
   220     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   221     do
   222       case "$REPLY" in
   223         \#* | "") ;;
   224         /*) init_component "$REPLY" ;;
   225         *) init_component "$BASE/$REPLY" ;;
   226       esac
   227     done
   228   } < "$CATALOG"
   229 }
   230 
   231 #main components
   232 init_component "$ISABELLE_HOME"
   233 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   234 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   235 
   236 
   237 #ML system identifier
   238 if [ -z "$ML_PLATFORM" ]; then
   239   ML_IDENTIFIER="$ML_SYSTEM"
   240 else
   241   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   242 fi
   243 
   244 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   245 
   246 #enforce JAVA_HOME
   247 export JAVA_HOME="$ISABELLE_JDK_HOME"
   248 
   249 #build condition etc.
   250 case "$ML_SYSTEM" in
   251   polyml*)
   252     ISABELLE_POLYML="true"
   253     ;;
   254   *)
   255     ISABELLE_POLYML=""
   256     ;;
   257 esac
   258 
   259 set +o allexport
   260 
   261 fi