# HG changeset patch
# User wenzelm
# Date 1345198498 -7200
# Node ID 623ba165d059b1c1ed3560b6735a0c8f9768cc27
# Parent  d1d806a42c919fd2ce34bccde1171b58c0123cea
direct support for component forests via init_components;
explicit ISABELLE_COMPONENTS_MISSING;

diff -r d1d806a42c91 -r 623ba165d059 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Fri Aug 17 11:42:05 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy	Fri Aug 17 12:14:58 2012 +0200
@@ -299,18 +299,18 @@
   For example, the following setting allows to refer to files within
   the component later on, without having to hardwire absolute paths:
 
-  \begin{ttbox}
-  MY_COMPONENT_HOME="$COMPONENT"
-  \end{ttbox}
+\begin{ttbox}
+MY_COMPONENT_HOME="$COMPONENT"
+\end{ttbox}
 
   Components can also add to existing Isabelle settings such as
   @{setting_def ISABELLE_TOOLS}, in order to provide
   component-specific tools that can be invoked by end-users.  For
   example:
 
-  \begin{ttbox}
-  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-  \end{ttbox}
+\begin{ttbox}
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+\end{ttbox}
 
   \item @{verbatim "etc/components"} holds a list of further
   sub-components of the same structure.  The directory specifications
@@ -328,12 +328,23 @@
   \verb,init_component, shell function in the \verb,etc/settings,
   script of \verb,$ISABELLE_HOME_USER, (or any other component
   directory).  For example:
-  \begin{verbatim}
-  if [ -d "$HOME/screwdriver-2.0" ]
-  then
-    init_component "$HOME/screwdriver-2.0"
-  else
-  \end{verbatim}
+\begin{ttbox}
+init_component "$HOME/screwdriver-2.0"
+\end{ttbox}
+
+  This is tolerant wrt.\ missing component directories, but might
+  produce a warning.
+
+  \medskip More complex situations may be addressed by initializing
+  components listed in a given catalog file, relatively to some base
+  directory:
+
+\begin{ttbox}
+init_components "$HOME/my_component_store" "some_catalog_file"
+\end{ttbox}
+
+  The component directories listed in the catalog file are treated as
+  relative to the given base directory.
 *}
 
 
diff -r d1d806a42c91 -r 623ba165d059 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 11:42:05 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 12:14:58 2012 +0200
@@ -310,18 +310,18 @@
   For example, the following setting allows to refer to files within
   the component later on, without having to hardwire absolute paths:
 
-  \begin{ttbox}
-  MY_COMPONENT_HOME="$COMPONENT"
-  \end{ttbox}
+\begin{ttbox}
+MY_COMPONENT_HOME="$COMPONENT"
+\end{ttbox}
 
   Components can also add to existing Isabelle settings such as
   \indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOLS}}}}}, in order to provide
   component-specific tools that can be invoked by end-users.  For
   example:
 
-  \begin{ttbox}
-  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-  \end{ttbox}
+\begin{ttbox}
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+\end{ttbox}
 
   \item \verb|etc/components| holds a list of further
   sub-components of the same structure.  The directory specifications
@@ -339,12 +339,23 @@
   \verb,init_component, shell function in the \verb,etc/settings,
   script of \verb,$ISABELLE_HOME_USER, (or any other component
   directory).  For example:
-  \begin{verbatim}
-  if [ -d "$HOME/screwdriver-2.0" ]
-  then
-    init_component "$HOME/screwdriver-2.0"
-  else
-  \end{verbatim}%
+\begin{ttbox}
+init_component "$HOME/screwdriver-2.0"
+\end{ttbox}
+
+  This is tolerant wrt.\ missing component directories, but might
+  produce a warning.
+
+  \medskip More complex situations may be addressed by initializing
+  components listed in a given catalog file, relatively to some base
+  directory:
+
+\begin{ttbox}
+init_components "$HOME/my_component_store" "some_catalog_file"
+\end{ttbox}
+
+  The component directories listed in the catalog file are treated as
+  relative to the given base directory.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r d1d806a42c91 -r 623ba165d059 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*)