1.1 --- a/etc/settings	Sun Aug 02 21:03:38 2009 +0200
     1.2 +++ b/etc/settings	Tue Aug 04 01:01:23 2009 +0200
     1.3 @@ -144,6 +144,7 @@
     1.4  # Site settings check -- just to make it a little bit harder to copy this file verbatim!
     1.5  [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
     1.6    { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
     1.7 +ISABELLE_SITE_SETTINGS_PRESENT=true
     1.8  
     1.9  
    1.10  ###

     2.1 --- a/lib/scripts/getsettings	Sun Aug 02 21:03:38 2009 +0200
     2.2 +++ b/lib/scripts/getsettings	Tue Aug 04 01:01:23 2009 +0200
     2.3 @@ -68,14 +68,43 @@
     2.4    done
     2.5  }
     2.6  
     2.7 -#get actual settings
     2.8 -source "$ISABELLE_HOME/etc/settings" || exit 2
     2.9 -ISABELLE_SITE_SETTINGS_PRESENT=true
    2.10 +#nested components
    2.11 +ISABELLE_COMPONENTS=""
    2.12 +function init_component ()
    2.13 +{
    2.14 +  local COMPONENT="$1"
    2.15 +
    2.16 +  if [ ! -d "$COMPONENT" ]; then
    2.17 +    echo >&2 "Bad Isabelle component: $COMPONENT"
    2.18 +    exit 2
    2.19 +  elif [ -z "$ISABELLE_COMPONENTS" ]; then
    2.20 +    ISABELLE_COMPONENTS="$COMPONENT"
    2.21 +  else
    2.22 +    ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    2.23 +  fi
    2.24 +  if [ -f "$COMPONENT/etc/settings" ]; then
    2.25 +    source "$COMPONENT/etc/settings" || exit 2
    2.26 +  fi
    2.27 +  if [ -f "$COMPONENT/etc/components" ]; then
    2.28 +    {
    2.29 +      while read; do
    2.30 +        case "$REPLY" in
    2.31 +          \#* | "") ;;
    2.32 +          /*) init_component "$REPLY" ;;
    2.33 +          *) init_component "$COMPONENT/$REPLY" ;;
    2.34 +        esac
    2.35 +      done
    2.36 +    } < "$COMPONENT/etc/components"
    2.37 +  fi
    2.38 +}
    2.39 +
    2.40 +#main components
    2.41 +init_component "$ISABELLE_HOME"
    2.42  
    2.43  [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
    2.44    { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
    2.45  [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
    2.46 -  { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
    2.47 +  init_component "$ISABELLE_HOME_USER"
    2.48  
    2.49  #ML system identifier
    2.50  if [ -z "$ML_PLATFORM" ]; then