# HG changeset patch
# User wenzelm
# Date 1335629119 -7200
# Node ID e6e1b670520b8c643360df109187e8075d5e4282
# Parent  13530d774a213d21e89a4fa560c48cbd9b6a3d8b
some coverage of isabelle env;

diff -r 13530d774a21 -r e6e1b670520b doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Sat Apr 28 17:54:50 2012 +0200
+++ b/doc-src/System/Thy/Misc.thy	Sat Apr 28 18:05:19 2012 +0200
@@ -51,6 +51,22 @@
 *}
 
 
+section {* Shell commands within the settings environment \label{sec:tool-env} *}
+
+text {* The @{tool_def env} utility is a direct wrapper for the
+  standard @{verbatim "/usr/bin/env"} command on POSIX systems,
+  running within the Isabelle settings environment
+  (\secref{sec:settings}).
+
+  The command-line arguments are that of the underlying version of
+  @{verbatim env}.  For example, the following invokes an instance of
+  the GNU Bash shell within the Isabelle environment:
+\begin{alltt}
+  isabelle env bash
+\end{alltt}
+*}
+
+
 section {* Getting logic images *}
 
 text {*
diff -r 13530d774a21 -r e6e1b670520b doc-src/System/Thy/document/Misc.tex
--- a/doc-src/System/Thy/document/Misc.tex	Sat Apr 28 17:54:50 2012 +0200
+++ b/doc-src/System/Thy/document/Misc.tex	Sat Apr 28 18:05:19 2012 +0200
@@ -73,6 +73,25 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Shell commands within the settings environment \label{sec:tool-env}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatt{env}}}}} utility is a direct wrapper for the
+  standard \verb|/usr/bin/env| command on POSIX systems,
+  running within the Isabelle settings environment
+  (\secref{sec:settings}).
+
+  The command-line arguments are that of the underlying version of
+  \verb|env|.  For example, the following invokes an instance of
+  the GNU Bash shell within the Isabelle environment:
+\begin{alltt}
+  isabelle env bash
+\end{alltt}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Getting logic images%
 }
 \isamarkuptrue%