doc-src/System/Thy/document/Misc.tex

 
   \medskip The \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCS}}}} setting specifies the list of
   directories (separated by colons) to be scanned for documentations.
   The program for viewing \verb|dvi| files is determined by the
   \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.%
+\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%
 }