# HG changeset patch
# User wenzelm
# Date 1259936730 -3600
# Node ID c3b822d234f42aa59237a172e8eb26b7aef559d3
# Parent  01dcd9b926bf22b54c1b436194c97a234cfc3b7f# Parent  5e9ddf000d97b86ef5d40a1a0e874bebe0e8f503
merged

diff -r 01dcd9b926bf -r c3b822d234f4 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Fri Dec 04 15:20:24 2009 +0100
+++ b/doc-src/System/Thy/Basics.thy	Fri Dec 04 15:25:30 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 01dcd9b926bf -r c3b822d234f4 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Fri Dec 04 15:20:24 2009 +0100
+++ b/doc-src/System/Thy/document/Basics.tex	Fri Dec 04 15:25:30 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%
 %