lib/scripts/getsettings
author wenzelm
Sat Apr 17 21:01:55 2010 +0200 (2010-04-17)
changeset 36194 8e61560ded89
parent 34257 b5176fd9ab3c
child 36196 cbb9ee265cdd
permissions -rw-r--r--
THIS_CYGWIN;
     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 #Isabelle distribution identifier -- filled in automatically!
    31 ISABELLE_IDENTIFIER=""
    32 
    33 #users tend to put strange things in here ...
    34 unset ENV
    35 unset BASH_ENV
    36 
    37 #support easy settings
    38 function choosefrom ()
    39 {
    40   local RESULT=""
    41   local FILE=""
    42 
    43   for FILE in "$@"
    44   do
    45     [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
    46   done
    47 
    48   [ -z "$RESULT" ] && RESULT="$FILE"
    49   echo "$RESULT"
    50 }
    51 
    52 #JVM path wrapper
    53 if [ "$OSTYPE" = cygwin ]; then
    54   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
    55   function jvmpath() { cygpath -w -p "$@"; }
    56   THIS_CYGWIN="$(jvmpath "/")"
    57 else
    58   function jvmpath() { echo "$@"; }
    59 fi
    60 HOME_JVM="$HOME"
    61 
    62 #CLASSPATH convenience
    63 function classpath () {
    64   for X in "$@"
    65   do
    66     if [ -z "$CLASSPATH" ]; then
    67       CLASSPATH="$X"
    68     else
    69       CLASSPATH="$CLASSPATH:$X"
    70     fi
    71   done
    72 }
    73 
    74 #arrays
    75 function splitarray ()
    76 {
    77   SPLITARRAY=()
    78   local IFS="$1"; shift
    79   for X in $*
    80   do
    81     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
    82   done
    83 }
    84 
    85 #nested components
    86 ISABELLE_COMPONENTS=""
    87 function init_component ()
    88 {
    89   local COMPONENT="$1"
    90 
    91   if [ ! -d "$COMPONENT" ]; then
    92     echo >&2 "Bad Isabelle component: \"$COMPONENT\""
    93     exit 2
    94   elif [ -z "$ISABELLE_COMPONENTS" ]; then
    95     ISABELLE_COMPONENTS="$COMPONENT"
    96   else
    97     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    98   fi
    99   if [ -f "$COMPONENT/etc/settings" ]; then
   100     source "$COMPONENT/etc/settings" || exit 2
   101   fi
   102   if [ -f "$COMPONENT/etc/components" ]; then
   103     {
   104       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   105       do
   106         case "$REPLY" in
   107           \#* | "") ;;
   108           /*) init_component "$REPLY" ;;
   109           *) init_component "$COMPONENT/$REPLY" ;;
   110         esac
   111       done
   112     } < "$COMPONENT/etc/components"
   113   fi
   114 }
   115 
   116 #main components
   117 init_component "$ISABELLE_HOME"
   118 
   119 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
   120   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
   121 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   122 
   123 #ML system identifier
   124 if [ -z "$ML_PLATFORM" ]; then
   125   ML_IDENTIFIER="$ML_SYSTEM"
   126 else
   127   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   128 fi
   129 
   130 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   131 
   132 set +o allexport
   133 
   134 fi