--- a/doc-src/System/Thy/Basics.thy Wed Aug 15 11:04:56 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy Wed Aug 15 11:41:27 2012 +0200
@@ -27,7 +27,7 @@
of the actual ML system to be used. Regular users rarely need to
care about the low-level process.
- \item The main \emph{Isabelle tools wrapper} (@{executable_ref
+ \item The main \emph{Isabelle tool wrapper} (@{executable_ref
isabelle}) provides a generic startup environment Isabelle related
utilities, user interfaces etc. Such tools automatically benefit
from the settings mechanism.
@@ -491,7 +491,7 @@
*}
-section {* The Isabelle tools wrapper \label{sec:isabelle-tool} *}
+section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
text {*
All Isabelle related tools and interfaces are called via a common
@@ -520,9 +520,8 @@
subsubsection {* Examples *}
-text {*
- Show the list of available documentation of the current Isabelle
- installation like this:
+text {* Show the list of available documentation of the Isabelle
+ distribution:
\begin{ttbox}
isabelle doc
@@ -533,14 +532,10 @@
isabelle doc system
\end{ttbox}
- Create an Isabelle session derived from HOL (see also
- \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
+ Query the Isabelle settings environment:
\begin{ttbox}
- isabelle mkdir HOL Test && isabelle make
+ isabelle getenv ISABELLE_HOME_USER
\end{ttbox}
- Note that @{verbatim "isabelle mkdir"} is usually only invoked once;
- existing sessions (including document output etc.) are then updated
- by @{verbatim "isabelle make"} alone.
*}
end
\ No newline at end of file
--- a/doc-src/System/Thy/document/Basics.tex Wed Aug 15 11:04:56 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Wed Aug 15 11:41:27 2012 +0200
@@ -45,7 +45,7 @@
of the actual ML system to be used. Regular users rarely need to
care about the low-level process.
- \item The main \emph{Isabelle tools wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}) provides a generic startup environment Isabelle related
+ \item The main \emph{Isabelle tool wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}) provides a generic startup environment Isabelle related
utilities, user interfaces etc. Such tools automatically benefit
from the settings mechanism.
@@ -505,7 +505,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}%
+\isamarkupsection{The Isabelle tool wrapper \label{sec:isabelle-tool}%
}
\isamarkuptrue%
%
@@ -538,8 +538,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Show the list of available documentation of the current Isabelle
- installation like this:
+Show the list of available documentation of the Isabelle
+ distribution:
\begin{ttbox}
isabelle doc
@@ -550,14 +550,10 @@
isabelle doc system
\end{ttbox}
- Create an Isabelle session derived from HOL (see also
- \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
+ Query the Isabelle settings environment:
\begin{ttbox}
- isabelle mkdir HOL Test && isabelle make
-\end{ttbox}
- Note that \verb|isabelle mkdir| is usually only invoked once;
- existing sessions (including document output etc.) are then updated
- by \verb|isabelle make| alone.%
+ isabelle getenv ISABELLE_HOME_USER
+\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%