some coverage of isabelle env;
authorwenzelm
Sat Apr 28 18:05:19 2012 +0200 (2012-04-28)
changeset 47828e6e1b670520b
parent 47827 13530d774a21
child 47829 0e36cc70cb3e
some coverage of isabelle env;
doc-src/System/Thy/Misc.thy
doc-src/System/Thy/document/Misc.tex
     1.1 --- a/doc-src/System/Thy/Misc.thy	Sat Apr 28 17:54:50 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Misc.thy	Sat Apr 28 18:05:19 2012 +0200
     1.3 @@ -51,6 +51,22 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +section {* Shell commands within the settings environment \label{sec:tool-env} *}
     1.8 +
     1.9 +text {* The @{tool_def env} utility is a direct wrapper for the
    1.10 +  standard @{verbatim "/usr/bin/env"} command on POSIX systems,
    1.11 +  running within the Isabelle settings environment
    1.12 +  (\secref{sec:settings}).
    1.13 +
    1.14 +  The command-line arguments are that of the underlying version of
    1.15 +  @{verbatim env}.  For example, the following invokes an instance of
    1.16 +  the GNU Bash shell within the Isabelle environment:
    1.17 +\begin{alltt}
    1.18 +  isabelle env bash
    1.19 +\end{alltt}
    1.20 +*}
    1.21 +
    1.22 +
    1.23  section {* Getting logic images *}
    1.24  
    1.25  text {*
     2.1 --- a/doc-src/System/Thy/document/Misc.tex	Sat Apr 28 17:54:50 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Misc.tex	Sat Apr 28 18:05:19 2012 +0200
     2.3 @@ -73,6 +73,25 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 +\isamarkupsection{Shell commands within the settings environment \label{sec:tool-env}%
     2.8 +}
     2.9 +\isamarkuptrue%
    2.10 +%
    2.11 +\begin{isamarkuptext}%
    2.12 +The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatt{env}}}}} utility is a direct wrapper for the
    2.13 +  standard \verb|/usr/bin/env| command on POSIX systems,
    2.14 +  running within the Isabelle settings environment
    2.15 +  (\secref{sec:settings}).
    2.16 +
    2.17 +  The command-line arguments are that of the underlying version of
    2.18 +  \verb|env|.  For example, the following invokes an instance of
    2.19 +  the GNU Bash shell within the Isabelle environment:
    2.20 +\begin{alltt}
    2.21 +  isabelle env bash
    2.22 +\end{alltt}%
    2.23 +\end{isamarkuptext}%
    2.24 +\isamarkuptrue%
    2.25 +%
    2.26  \isamarkupsection{Getting logic images%
    2.27  }
    2.28  \isamarkuptrue%