
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.




