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. *}