--- 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}
*}
--- a/doc-src/System/Thy/document/Basics.tex Tue Nov 16 20:30:25 2010 +0100
+++ b/doc-src/System/Thy/document/Basics.tex Tue Nov 16 21:48:14 2010 +0100
@@ -318,12 +318,18 @@
The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
itself. After initializing all of its sub-components recursively,
\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to \verb|$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 \verb|$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}%
\end{isamarkuptext}%
\isamarkuptrue%
%