lib/scripts/getsettings

 
 set -o allexport
 
 ISABELLE_SETTINGS_PRESENT=true
 
-#Cygwin vs Posix
+#Cygwin vs. POSIX
 if [ "$OSTYPE" = cygwin ]
 then
   if [ -z "$USER_HOME" ]; then
     USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
   fi

   do
     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   done
 }
 
-#nested components
+
+# components
+
 ISABELLE_COMPONENTS=""
+ISABELLE_COMPONENTS_MISSING=""
+
+#init component tree
 function init_component ()
 {
   local COMPONENT="$1"
   case "$COMPONENT" in
     /*) ;;

       echo >&2 "Absolute component path required: \"$COMPONENT\""
       exit 2
       ;;
   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"
-  fi
+    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="$?"
     if [ "$RC" -ne 0 ]; then
       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
       exit 2
     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"
-  fi
+    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
 init_component "$ISABELLE_HOME"
 [ -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"
 else
   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*)
     ISABELLE_POLYML="true"