lib/scripts/getsettings

--- a/lib/scripts/getsettings	Fri Aug 17 11:42:05 2012 +0200
+++ b/lib/scripts/getsettings	Fri Aug 17 12:14:58 2012 +0200
@@ -11,7 +11,7 @@
 
 ISABELLE_SETTINGS_PRESENT=true
 
-#Cygwin vs Posix
+#Cygwin vs. POSIX
 if [ "$OSTYPE" = cygwin ]
 then
   if [ -z "$USER_HOME" ]; then
@@ -148,8 +148,13 @@
   done
 }
 
-#nested components
+
+# components
+
 ISABELLE_COMPONENTS=""
+ISABELLE_COMPONENTS_MISSING=""
+
+#init component tree
 function init_component ()
 {
   local COMPONENT="$1"
@@ -161,13 +166,21 @@
       ;;
   esac
 
-  if [ ! -d "$COMPONENT" ]; then
+  if [ -d "$COMPONENT" ]; then
+    if [ -z "$ISABELLE_COMPONENTS" ]; then
+      ISABELLE_COMPONENTS="$COMPONENT"
+    else
+      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+    fi
+  else
     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
-  elif [ -z "$ISABELLE_COMPONENTS" ]; then
-    ISABELLE_COMPONENTS="$COMPONENT"
-  else
-    ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
+      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
+    else
+      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
+    fi
   fi
+
   if [ -f "$COMPONENT/etc/settings" ]; then
     source "$COMPONENT/etc/settings"
     local RC="$?"
@@ -177,17 +190,34 @@
     fi
   fi
   if [ -f "$COMPONENT/etc/components" ]; then
-    {
-      while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
-      do
-        case "$REPLY" in
-          \#* | "") ;;
-          /*) init_component "$REPLY" ;;
-          *) init_component "$COMPONENT/$REPLY" ;;
-        esac
-      done
-    } < "$COMPONENT/etc/components"
+    init_components "$COMPONENT" "$COMPONENT/etc/components"
+  fi
+}
+
+#init component forest
+function init_components ()
+{
+  local BASE="$1"
+  local CATALOG="$2"
+
+  if [ ! -d "$BASE" ]; then
+    echo >&2 "Bad component base directory: \"$BASE\""
+    exit 2
   fi
+  if [ ! -f "$CATALOG" ]; then
+    echo >&2 "Bad component catalog file: \"$CATALOG\""
+    exit 2
+  fi
+  {
+    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+    do
+      case "$REPLY" in
+        \#* | "") ;;
+        /*) init_component "$REPLY" ;;
+        *) init_component "$BASE/$REPLY" ;;
+      esac
+    done
+  } < "$CATALOG"
 }
 
 #main components
@@ -195,6 +225,7 @@
 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
 
+
 #ML system identifier
 if [ -z "$ML_PLATFORM" ]; then
   ML_IDENTIFIER="$ML_SYSTEM"
@@ -202,11 +233,11 @@
   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
 fi
 
+ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
+
 #enforce JAVA_HOME
 export JAVA_HOME="$ISABELLE_JDK_HOME"
 
-ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
-
 #build condition etc.
 case "$ML_SYSTEM" in
   polyml*)