--- a/doc-src/System/Thy/Basics.thy Fri Dec 04 11:44:57 2009 +0100
+++ b/doc-src/System/Thy/Basics.thy Fri Dec 04 12:17:38 2009 +0100
@@ -298,6 +298,10 @@
@{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.
*}
--- a/doc-src/System/Thy/document/Basics.tex Fri Dec 04 11:44:57 2009 +0100
+++ b/doc-src/System/Thy/document/Basics.tex Fri Dec 04 12:17:38 2009 +0100
@@ -308,7 +308,11 @@
itself. After initializing all of its sub-components recursively,
\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\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|.%
+ 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%