--- a/doc-src/System/Thy/document/Misc.tex Fri Aug 17 17:52:10 2012 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Fri Aug 17 17:35:07 2012 +0200
@@ -28,6 +28,51 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Resolving Isabelle components \label{sec:tool-components}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{components}\hypertarget{tool.components}{\hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}}} tool resolves Isabelle components:
+\begin{ttbox}
+Usage: isabelle components [OPTIONS] [COMPONENTS ...]
+
+ Options are:
+ -R URL component repository
+ (default $ISABELLE_COMPONENT_REPOSITORY)
+ -a all missing components
+ -l list status
+
+ Resolve Isabelle components via download and installation.
+ COMPONENTS are identified via base name.
+
+ ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
+\end{ttbox}
+
+ Components are initialized as described in \secref{sec:components}
+ in a permissive manner, which can mark components as ``missing''.
+ This state is amended by letting \hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}} download and
+ unpack components that are published on the default component
+ repository \url{http://isabelle.in.tum.de/components/} in
+ particular.
+
+ Option \verb|-R| specifies an alternative component
+ repository. Note that \verb|file:///| URLs can be used for
+ local directories.
+
+ Option \verb|-a| selects all missing components to be
+ installed. Explicit components may be named as command
+ line-arguments as well. Note that components are uniquely
+ identified by their base name, while the installation takes place in
+ the location that was specified in the attempt to initialize the
+ component before.
+
+ Option \verb|-l| lists the current state of available and
+ missing components with their location (full name) within the
+ file-system.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Displaying documents%
}
\isamarkuptrue%