lib/scripts/getsettings
changeset 48838 623ba165d059
parent 48837 d1d806a42c91
child 49000 0cebcbeac4c7
     1.1 --- a/lib/scripts/getsettings	Fri Aug 17 11:42:05 2012 +0200
     1.2 +++ b/lib/scripts/getsettings	Fri Aug 17 12:14:58 2012 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  ISABELLE_SETTINGS_PRESENT=true
     1.6  
     1.7 -#Cygwin vs Posix
     1.8 +#Cygwin vs. POSIX
     1.9  if [ "$OSTYPE" = cygwin ]
    1.10  then
    1.11    if [ -z "$USER_HOME" ]; then
    1.12 @@ -148,8 +148,13 @@
    1.13    done
    1.14  }
    1.15  
    1.16 -#nested components
    1.17 +
    1.18 +# components
    1.19 +
    1.20  ISABELLE_COMPONENTS=""
    1.21 +ISABELLE_COMPONENTS_MISSING=""
    1.22 +
    1.23 +#init component tree
    1.24  function init_component ()
    1.25  {
    1.26    local COMPONENT="$1"
    1.27 @@ -161,13 +166,21 @@
    1.28        ;;
    1.29    esac
    1.30  
    1.31 -  if [ ! -d "$COMPONENT" ]; then
    1.32 +  if [ -d "$COMPONENT" ]; then
    1.33 +    if [ -z "$ISABELLE_COMPONENTS" ]; then
    1.34 +      ISABELLE_COMPONENTS="$COMPONENT"
    1.35 +    else
    1.36 +      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    1.37 +    fi
    1.38 +  else
    1.39      echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
    1.40 -  elif [ -z "$ISABELLE_COMPONENTS" ]; then
    1.41 -    ISABELLE_COMPONENTS="$COMPONENT"
    1.42 -  else
    1.43 -    ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    1.44 +    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
    1.45 +      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
    1.46 +    else
    1.47 +      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
    1.48 +    fi
    1.49    fi
    1.50 +
    1.51    if [ -f "$COMPONENT/etc/settings" ]; then
    1.52      source "$COMPONENT/etc/settings"
    1.53      local RC="$?"
    1.54 @@ -177,17 +190,34 @@
    1.55      fi
    1.56    fi
    1.57    if [ -f "$COMPONENT/etc/components" ]; then
    1.58 -    {
    1.59 -      while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    1.60 -      do
    1.61 -        case "$REPLY" in
    1.62 -          \#* | "") ;;
    1.63 -          /*) init_component "$REPLY" ;;
    1.64 -          *) init_component "$COMPONENT/$REPLY" ;;
    1.65 -        esac
    1.66 -      done
    1.67 -    } < "$COMPONENT/etc/components"
    1.68 +    init_components "$COMPONENT" "$COMPONENT/etc/components"
    1.69 +  fi
    1.70 +}
    1.71 +
    1.72 +#init component forest
    1.73 +function init_components ()
    1.74 +{
    1.75 +  local BASE="$1"
    1.76 +  local CATALOG="$2"
    1.77 +
    1.78 +  if [ ! -d "$BASE" ]; then
    1.79 +    echo >&2 "Bad component base directory: \"$BASE\""
    1.80 +    exit 2
    1.81    fi
    1.82 +  if [ ! -f "$CATALOG" ]; then
    1.83 +    echo >&2 "Bad component catalog file: \"$CATALOG\""
    1.84 +    exit 2
    1.85 +  fi
    1.86 +  {
    1.87 +    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    1.88 +    do
    1.89 +      case "$REPLY" in
    1.90 +        \#* | "") ;;
    1.91 +        /*) init_component "$REPLY" ;;
    1.92 +        *) init_component "$BASE/$REPLY" ;;
    1.93 +      esac
    1.94 +    done
    1.95 +  } < "$CATALOG"
    1.96  }
    1.97  
    1.98  #main components
    1.99 @@ -195,6 +225,7 @@
   1.100  [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   1.101  [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   1.102  
   1.103 +
   1.104  #ML system identifier
   1.105  if [ -z "$ML_PLATFORM" ]; then
   1.106    ML_IDENTIFIER="$ML_SYSTEM"
   1.107 @@ -202,11 +233,11 @@
   1.108    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   1.109  fi
   1.110  
   1.111 +ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   1.112 +
   1.113  #enforce JAVA_HOME
   1.114  export JAVA_HOME="$ISABELLE_JDK_HOME"
   1.115  
   1.116 -ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   1.117 -
   1.118  #build condition etc.
   1.119  case "$ML_SYSTEM" in
   1.120    polyml*)