# HG changeset patch
# User wenzelm
# Date 1345217707 -7200
# Node ID 6408fb6f7d81241ceb119c3fb02069a80e4d3f9d
# Parent  9055bf115e30423a55fc22c526c4a92cef4b3b2e
some explanations on isabelle components;

diff -r 9055bf115e30 -r 6408fb6f7d81 NEWS
--- a/NEWS	Fri Aug 17 17:52:10 2012 +0200
+++ b/NEWS	Fri Aug 17 17:35:07 2012 +0200
@@ -106,6 +106,10 @@
 with "isabelle build", similar to former "isabelle mkdir" for
 "isabelle usedir".
 
+* The "isabelle components" tool helps to resolve add-on components
+that are not bundled, or referenced from a bare-bones repository
+version of Isabelle.
+
 * Discontinued support for Poly/ML 5.2.1, which was the last version
 without exception positions and advanced ML compiler/toplevel
 configuration.
diff -r 9055bf115e30 -r 6408fb6f7d81 README_REPOSITORY
--- a/README_REPOSITORY	Fri Aug 17 17:52:10 2012 +0200
+++ b/README_REPOSITORY	Fri Aug 17 17:35:07 2012 +0200
@@ -233,28 +233,34 @@
 Building a repository version of Isabelle
 -----------------------------------------
 
-A proper Isabelle distribution contains many add-on components that
-are important for practical use.  Some extra configuration is required
-to approximate this system integration from a bare-bones repository
-snapshot; see also its directory Admin/ (which is absent in official
-releases).
+The regular "isabelle build" tool allows to build session images as
+usual, but this first requires to resolve add-on components first,
+including the ML system.  Some extra configuration is required to
+approximate some of the system integration of official Isabelle
+releases from a bare-bones repository snapshot.  The special directory
+Admin/ -- which is absent in official releases -- might provide some
+further clues.
 
-  (1) Admin/components lists potentially relevant components, with
-    explicit version information for the given repository version.
-    For example, this allows to bisect over Mercurial history while
-    the contributing components change accordingly.
+Here is a reasonably easy way to include important Isabelle components
+on the spot:
+
+  (1) The bash script ISABELLE_HOME_USER/etc/settings is augmented by
+  some shell function invocations like this:
 
-  (2) Admin/init_components is a bash script that can be sourced in
-    $ISABELLE_HOME_USER/etc/settings to initialize components listed
-    in Admin/components and present in $ISABELLE_HOME_USER/contrib/.
+      init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
+      init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
+
+  This uses some central place "$HOME/.isabelle/contrib" to keep
+  component directories that are shared by all Isabelle versions.
+
+  (2) Missing components are resolved on the command line like this:
 
-  (3) http://isabelle.in.tum.de/components/ provides tar.gz archives
-    of many components, excluding some non-free ones (which are also
-    not part of Isabelle releases).
+      isabelle components -a
+
+  This will saturate the "$HOME/.isabelle/contrib" directory structure
+  from according to $ISABELLE_COMPONENT_REPOSITORY.
 
-Also note that the repository lacks some textual version identifiers
-in the sources and scripts; this implies some changed behavior when
-processing settings etc. -- especially the location of
-$ISABELLE_HOME_USER provided by the system.
-
-The isabelle build tool allows to build logic images.
+Since the given component catalogs in $ISABELLE_HOME/Admin/components
+are subject to the Mercurial history, it is possible to bisect over a
+range of Isabelle versions while references to the contributing
+components change accordingly.
diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Fri Aug 17 17:52:10 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy	Fri Aug 17 17:35:07 2012 +0200
@@ -345,6 +345,10 @@
 
   The component directories listed in the catalog file are treated as
   relative to the given base directory.
+
+  See also \secref{sec:tool-components} for some tool-support for
+  resolving components that are formally initialized but not installed
+  yet.
 *}
 
 
diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Fri Aug 17 17:52:10 2012 +0200
+++ b/doc-src/System/Thy/Misc.thy	Fri Aug 17 17:35:07 2012 +0200
@@ -10,6 +10,48 @@
 *}
 
 
+section {* Resolving Isabelle components \label{sec:tool-components} *}
+
+text {*
+  The @{tool_def 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 @{tool "components"} download and
+  unpack components that are published on the default component
+  repository \url{http://isabelle.in.tum.de/components/} in
+  particular.
+
+  Option @{verbatim "-R"} specifies an alternative component
+  repository.  Note that @{verbatim "file:///"} URLs can be used for
+  local directories.
+
+  Option @{verbatim "-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 @{verbatim "-l"} lists the current state of available and
+  missing components with their location (full name) within the
+  file-system.  *}
+
+
 section {* Displaying documents *}
 
 text {* The @{tool_def display} tool displays documents in DVI or PDF
diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 17:52:10 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 17:35:07 2012 +0200
@@ -355,7 +355,11 @@
 \end{ttbox}
 
   The component directories listed in the catalog file are treated as
-  relative to the given base directory.%
+  relative to the given base directory.
+
+  See also \secref{sec:tool-components} for some tool-support for
+  resolving components that are formally initialized but not installed
+  yet.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/document/Misc.tex
--- 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%