diff -r d95d209ae1c2 -r 636322bfd057 doc-src/System/basics.tex --- a/doc-src/System/basics.tex Wed May 21 17:11:24 1997 +0200 +++ b/doc-src/System/basics.tex Wed May 21 17:11:46 1997 +0200 @@ -55,10 +55,11 @@ In particular, we avoid the typical situation where prospective users of a software package are told to put this and that in their shell -startup scripts. Isabelle requires none such administrative chores of -its end-users --- the executables can be run straight away. Usually, -users would want to put the Isabelle \texttt{bin} directory into their -shell's search path, of course. +startup scripts, before being able to actually run it. Isabelle +requires none such administrative chores of its end-users --- the +executables can be invoked straight away. Usually, users would just +want to put the Isabelle \texttt{bin} directory into their shell's +search path, of course. \subsection{Building the environment} @@ -78,11 +79,11 @@ \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script with the auto-export option for variables enabled. - This file typically contains a rather long list of assigments - \texttt{FOO="bar"}, thus providing the site-wide default settings. - The Isabelle distribution already contains a global settings file - with sensible defaults for most variables. When installing the - system, only a few of these have to be adapted (most likely + This file typically contains a rather long list of shell variable + assigments, thus providing the site-wide default settings. The + Isabelle distribution already contains a global settings file with + sensible defaults for most variables. When installing the system, + only a few of these have to be adapted (most likely \texttt{ML_SYSTEM} etc.). \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it @@ -92,9 +93,9 @@ Thus individual users may override the site-wide defaults. See also file \texttt{etc/user-settings.sample} in the distribution. - Typically, user settings are a few lines only, just containing the - assigments that are really needed. One should definitely \emph{not} - start with a full copy the central + Typically, user settings should be a few lines only, just containing + the assigments that are really needed. One should definitely + \emph{not} start with a full copy the central \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very annoying maintainance problems later, when the Isabelle installation is updated or changed otherwise. @@ -171,8 +172,8 @@ \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is given explicitely by the user --- e.g.\ when running \texttt{isabelle} directly, or some user interface. - -\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitely prefixed to the + +\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command line of any \texttt{isatool usedir} invocation (see also \S\ref{sec:tool-usedir}). This typically contains compilation options for object-logics --- \texttt{usedir} is the basic utility @@ -224,11 +225,11 @@ \end{ttbox} Input files without path specifications are looked up in the \texttt{ISABELLE_PATH} setting, which may consist of multiple -components separated by colons --- these are tried in order. Short -output names are relative to the directory specified by -\texttt{ISABELLE_OUTPUT} setting. In any case, actual file locations -may also be given by including at least one \texttt{/} in the name -(hint: use \texttt{./} to refer to the current directory). +components separated by colons --- these are tried in order. +Likewise, short output names are relative to the directory specified +by \texttt{ISABELLE_OUTPUT}. In any case, actual file locations may +also be given by including at least one \texttt{/} in the name (hint: +use \texttt{./} to refer to the current directory). \subsection*{Options} @@ -254,9 +255,7 @@ \medskip The \texttt{-m} option adds identifiers of print modes to be made active for this session. Typically, this is used by some user interface, for example to enable output of mathematical symbols from a -special screen font. See also \S\ref{sec:tool-installfonts} about -fonts and the \emph{Isabelle Reference Manual} about print modes in -general. +special screen font. \medskip Isabelle normally enters an interactice {\ML} top-level loop (after processing the \texttt{-e} texts). The \texttt{-q} option @@ -292,7 +291,7 @@ isabelle -r Foo \end{ttbox} One may also use something like \texttt{chmod~-w} on the logic image -to have them read-only automatically. +to have it read-only automatically. \medskip The next example demonstrates batch execution of Isabelle. We print a certain theorem of \texttt{FOL}: @@ -305,8 +304,58 @@ \section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool} -FIXME +All Isabelle related utilities are called via a common wrapper --- +\ttindex{isatool}: +\begin{ttbox} +Usage: isatool TOOL [ARGS ...] + + Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL + for more specific help. + + Available tools are: + + doc - view Isabelle documentation + \(\vdots\) +\end{ttbox} +Basically, Isabelle tools are ordinary executable scripts. These are +run within the same settings environment as Isabelle proper, though, +see \S\ref{sec:settings}. The set of available tools is collected by +isatool from the directories listed in the \texttt{ISABELLE_TOOLS} +setting. Do not try to call the scripts directly. Neither should you +add the tools directories to your shell's search path. + + +\medskip See chapter~\ref{ch:tools} for descriptions of most utilities +that come with the Isabelle distributions. Third-parties may add their +own, of course. + \section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface} -FIXME +Isabelle is a generic theorem prover, even w.r.t.\ its user interface. +The \ttindex{Isabelle} command (note the capital \texttt{I}) provides +a uniform way for end-users to invoke a certain interface. Which one +to actually start is determined by the \settdx{ISABELLE_INTERFACE} +setting variable. Currently, the following are recognized: +\begin{ttdescription} +\item[none] is just a pass-through to \texttt{isabelle}. Thus + \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}. + +\item[xterm] refers to a simple xterm-based interface which is part of + the Isabelle distribution. + +\item[emacs] refers to David Aspinall's \emph{Isamode} for emacs. + Isabelle just provides a wrapper for this, the actual Isamode + distribution is available elsewhere. +\end{ttdescription} + +The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}. +This interface runs \texttt{isabelle} within its own xterm window. +Usually, display of mathematical symbols from the Isabelle font is +also enabled (see \S\ref{sec:tool-installfonts} for font configuration +issues). Furthermore, different kinds of identifiers in logical terms +are highlighted appropriately, e.g.\ free variables in bold and bound +variables underlined. + +There are some more options available. Just pass \texttt{-?} to the +\texttt{xterm} interface to have its usage printed.