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