lib/scripts/getsettings
author wenzelm
Tue Nov 16 21:54:52 2010 +0100 (2010-11-16)
changeset 40570 bf8f92bdf630
parent 40568 3003be923908
child 41511 2fe62d602681
permissions -rw-r--r--
init_component: require absolute path (when invoked by user scripts);
     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 export ISABELLE_HOME
    15 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
    16 then
    17   echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
    18   echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    19 fi
    20 
    21 #key executables
    22 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    23 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    24 
    25 function isabelle ()
    26 {
    27   "$ISABELLE_TOOL" "$@"
    28 }
    29 
    30 #platform
    31 . "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    32 
    33 #Isabelle distribution identifier -- filled in automatically!
    34 ISABELLE_IDENTIFIER=""
    35 
    36 #users tend to put strange things in here ...
    37 unset ENV
    38 unset BASH_ENV
    39 
    40 #support easy settings
    41 function choosefrom ()
    42 {
    43   local RESULT=""
    44   local FILE=""
    45 
    46   for FILE in "$@"
    47   do
    48     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    49   done
    50 
    51   [ -z "$RESULT" ] && RESULT="$FILE"
    52   echo "$RESULT"
    53 }
    54 
    55 #JVM path wrapper
    56 if [ "$OSTYPE" = cygwin ]; then
    57   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
    58   function jvmpath() { cygpath -w -p "$@"; }
    59   THIS_CYGWIN="$(jvmpath "/")"
    60 else
    61   function jvmpath() { echo "$@"; }
    62 fi
    63 HOME_JVM="$HOME"
    64 
    65 #CLASSPATH convenience
    66 function classpath () {
    67   for X in "$@"
    68   do
    69     if [ -z "$CLASSPATH" ]; then
    70       CLASSPATH="$X"
    71     else
    72       CLASSPATH="$CLASSPATH:$X"
    73     fi
    74   done
    75   export CLASSPATH
    76 }
    77 
    78 #arrays
    79 function splitarray ()
    80 {
    81   SPLITARRAY=()
    82   local IFS="$1"; shift
    83   for X in $*
    84   do
    85     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
    86   done
    87 }
    88 
    89 #nested components
    90 ISABELLE_COMPONENTS=""
    91 function init_component ()
    92 {
    93   local COMPONENT="$1"
    94   case "$COMPONENT" in
    95     /*) ;;
    96     *)
    97       echo >&2 "Absolute component path required: \"$COMPONENT\""
    98       exit 2
    99       ;;
   100   esac
   101 
   102   if [ ! -d "$COMPONENT" ]; then
   103     echo >&2 "Bad Isabelle component: \"$COMPONENT\""
   104     exit 2
   105   elif [ -z "$ISABELLE_COMPONENTS" ]; then
   106     ISABELLE_COMPONENTS="$COMPONENT"
   107   else
   108     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   109   fi
   110   if [ -f "$COMPONENT/etc/settings" ]; then
   111     source "$COMPONENT/etc/settings" || exit 2
   112   fi
   113   if [ -f "$COMPONENT/etc/components" ]; then
   114     {
   115       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   116       do
   117         case "$REPLY" in
   118           \#* | "") ;;
   119           /*) init_component "$REPLY" ;;
   120           *) init_component "$COMPONENT/$REPLY" ;;
   121         esac
   122       done
   123     } < "$COMPONENT/etc/components"
   124   fi
   125 }
   126 
   127 #main components
   128 init_component "$ISABELLE_HOME"
   129 
   130 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
   131   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
   132 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   133 
   134 #ML system identifier
   135 if [ -z "$ML_PLATFORM" ]; then
   136   ML_IDENTIFIER="$ML_SYSTEM"
   137 else
   138   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   139 fi
   140 
   141 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   142 
   143 set +o allexport
   144 
   145 fi