# HG changeset patch
# User wenzelm
# Date 1249340483 -7200
# Node ID c5523ded51d9b5fded52227c345336e539f0084c
# Parent  df010136264df7a0335c7ba9fb530c1999c177b1
basic support for components (which imitate the usual Isabelle directory layout);

diff -r df010136264d -r c5523ded51d9 etc/settings
--- a/etc/settings	Sun Aug 02 21:03:38 2009 +0200
+++ b/etc/settings	Tue Aug 04 01:01:23 2009 +0200
@@ -144,6 +144,7 @@
 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
   { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
+ISABELLE_SITE_SETTINGS_PRESENT=true
 
 
 ###
diff -r df010136264d -r c5523ded51d9 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sun Aug 02 21:03:38 2009 +0200
+++ b/lib/scripts/getsettings	Tue Aug 04 01:01:23 2009 +0200
@@ -68,14 +68,43 @@
   done
 }
 
-#get actual settings
-source "$ISABELLE_HOME/etc/settings" || exit 2
-ISABELLE_SITE_SETTINGS_PRESENT=true
+#nested components
+ISABELLE_COMPONENTS=""
+function init_component ()
+{
+  local COMPONENT="$1"
+
+  if [ ! -d "$COMPONENT" ]; then
+    echo >&2 "Bad Isabelle component: $COMPONENT"
+    exit 2
+  elif [ -z "$ISABELLE_COMPONENTS" ]; then
+    ISABELLE_COMPONENTS="$COMPONENT"
+  else
+    ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+  fi
+  if [ -f "$COMPONENT/etc/settings" ]; then
+    source "$COMPONENT/etc/settings" || exit 2
+  fi
+  if [ -f "$COMPONENT/etc/components" ]; then
+    {
+      while read; do
+        case "$REPLY" in
+          \#* | "") ;;
+          /*) init_component "$REPLY" ;;
+          *) init_component "$COMPONENT/$REPLY" ;;
+        esac
+      done
+    } < "$COMPONENT/etc/components"
+  fi
+}
+
+#main components
+init_component "$ISABELLE_HOME"
 
 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
 [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
-  { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
+  init_component "$ISABELLE_HOME_USER"
 
 #ML system identifier
 if [ -z "$ML_PLATFORM" ]; then