# HG changeset patch
# User wenzelm
# Date 1289940494 -3600
# Node ID ffcff7509a499780979ec7f269188e86b8f997cd
# Parent  3003be92390877302bc04d35669e6b884b14da88
more explicit explanation of init_component shell function;

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