--- a/doc-src/System/Thy/Basics.thy Tue Nov 16 20:30:25 2010 +0100
+++ b/doc-src/System/Thy/Basics.thy Tue Nov 16 21:48:14 2010 +0100
@@ -309,12 +309,18 @@
The root of component initialization is @{setting ISABELLE_HOME}
itself. After initializing all of its sub-components recursively,
@{setting ISABELLE_HOME_USER} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
-
- It is also possible to initialize components programmatically via
- the \verb,init_component, shell function, say within the
- \verb,settings, script of another component.
+ that directory exists). This allows to install private components
+ via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+ often more convenient to do that programmatically via the
+ \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}
*}