direct support for component forests via init_components;
explicit ISABELLE_COMPONENTS_MISSING;
--- 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.
*}
--- 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%
%
--- 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*)