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