# HG changeset patch
# User wenzelm
# Date 1259925458 -3600
# Node ID 5e9ddf000d97b86ef5d40a1a0e874bebe0e8f503
# Parent  651028e34b5d82762f2bd9212d3b84f117d292df
document init_component shell function;

diff -r 651028e34b5d -r 5e9ddf000d97 doc-src/System/Thy/Basics.thy
--- 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.
 *}
 
 
diff -r 651028e34b5d -r 5e9ddf000d97 doc-src/System/Thy/document/Basics.tex
--- 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%
 %