1.1 --- a/lib/scripts/getsettings	Sun Aug 02 21:03:38 2009 +0200
     1.2 +++ b/lib/scripts/getsettings	Tue Aug 04 01:01:23 2009 +0200
     1.3 @@ -68,14 +68,43 @@
     1.4    done
     1.5  }
     1.6  
     1.7 -#get actual settings
     1.8 -source "$ISABELLE_HOME/etc/settings" || exit 2
     1.9 -ISABELLE_SITE_SETTINGS_PRESENT=true
    1.10 +#nested components
    1.11 +ISABELLE_COMPONENTS=""
    1.12 +function init_component ()
    1.13 +{
    1.14 +  local COMPONENT="$1"
    1.15 +
    1.16 +  if [ ! -d "$COMPONENT" ]; then
    1.17 +    echo >&2 "Bad Isabelle component: $COMPONENT"
    1.18 +    exit 2
    1.19 +  elif [ -z "$ISABELLE_COMPONENTS" ]; then
    1.20 +    ISABELLE_COMPONENTS="$COMPONENT"
    1.21 +  else
    1.22 +    ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    1.23 +  fi
    1.24 +  if [ -f "$COMPONENT/etc/settings" ]; then
    1.25 +    source "$COMPONENT/etc/settings" || exit 2
    1.26 +  fi
    1.27 +  if [ -f "$COMPONENT/etc/components" ]; then
    1.28 +    {
    1.29 +      while read; do
    1.30 +        case "$REPLY" in
    1.31 +          \#* | "") ;;
    1.32 +          /*) init_component "$REPLY" ;;
    1.33 +          *) init_component "$COMPONENT/$REPLY" ;;
    1.34 +        esac
    1.35 +      done
    1.36 +    } < "$COMPONENT/etc/components"
    1.37 +  fi
    1.38 +}
    1.39 +
    1.40 +#main components
    1.41 +init_component "$ISABELLE_HOME"
    1.42  
    1.43  [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
    1.44    { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
    1.45  [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
    1.46 -  { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
    1.47 +  init_component "$ISABELLE_HOME_USER"
    1.48  
    1.49  #ML system identifier
    1.50  if [ -z "$ML_PLATFORM" ]; then