diff -r 3003be923908 -r ffcff7509a49 doc-src/System/Thy/Basics.thy --- 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} *}