lib/scripts/getsettings
author wenzelm
Sat Apr 17 22:58:29 2010 +0200 (2010-04-17)
changeset 36196 cbb9ee265cdd
parent 36194 8e61560ded89
child 40568 3003be923908
permissions -rw-r--r--
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
     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 }
    76 
    77 #arrays
    78 function splitarray ()
    79 {
    80   SPLITARRAY=()
    81   local IFS="$1"; shift
    82   for X in $*
    83   do
    84     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
    85   done
    86 }
    87 
    88 #nested components
    89 ISABELLE_COMPONENTS=""
    90 function init_component ()
    91 {
    92   local COMPONENT="$1"
    93 
    94   if [ ! -d "$COMPONENT" ]; then
    95     echo >&2 "Bad Isabelle component: \"$COMPONENT\""
    96     exit 2
    97   elif [ -z "$ISABELLE_COMPONENTS" ]; then
    98     ISABELLE_COMPONENTS="$COMPONENT"
    99   else
   100     ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   101   fi
   102   if [ -f "$COMPONENT/etc/settings" ]; then
   103     source "$COMPONENT/etc/settings" || exit 2
   104   fi
   105   if [ -f "$COMPONENT/etc/components" ]; then
   106     {
   107       while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   108       do
   109         case "$REPLY" in
   110           \#* | "") ;;
   111           /*) init_component "$REPLY" ;;
   112           *) init_component "$COMPONENT/$REPLY" ;;
   113         esac
   114       done
   115     } < "$COMPONENT/etc/components"
   116   fi
   117 }
   118 
   119 #main components
   120 init_component "$ISABELLE_HOME"
   121 
   122 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
   123   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
   124 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   125 
   126 #ML system identifier
   127 if [ -z "$ML_PLATFORM" ]; then
   128   ML_IDENTIFIER="$ML_SYSTEM"
   129 else
   130   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   131 fi
   132 
   133 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   134 
   135 set +o allexport
   136 
   137 fi