--- a/doc-src/System/basics.tex Mon Oct 18 19:43:18 1999 +0200
+++ b/doc-src/System/basics.tex Tue Oct 19 13:45:51 1999 +0200
@@ -4,7 +4,7 @@
\chapter{The Isabelle system environment}
This manual describes Isabelle together with related tools and user interfaces
-as seen from an outside, system oriented view. See also the \emph{Isabelle
+as seen from an outside (system oriented) view. See also the \emph{Isabelle
Reference Manual}~\cite{isabelle-ref} and the \emph{Isabelle Isar Reference
Manual}~\cite{isabelle-isar-ref} for the actual Isabelle commands and
related functions.
@@ -48,17 +48,17 @@
In particular, we avoid the typical situation where prospective users of a
software package are told to put several things into their shell 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. Occasionally, users would still want to put the Isabelle
-\texttt{bin} directory into their shell's search path, but this is not
-required.
+scripts, before being able to actually run the program. Isabelle requires none
+such administrative chores of its end-users --- the executables can be invoked
+straight away.\footnote{Occasionally, users would still want to put the
+ Isabelle \texttt{bin} directory into their shell's search path, but this is
+ not required.}
\subsection{Creating the environment}
Whenever any of the Isabelle executables is run, their settings environment is
-built as follows:
+built as follows.
\begin{enumerate}
\item The special variable \settdx{ISABELLE_HOME} is determined automatically
@@ -66,7 +66,7 @@
You should not try to set \texttt{ISABELLE_HOME} manually. Also note that
the Isabelle executables either have to be run from their original location
- in the distribution directory, or via the executable objects created via the
+ in the distribution directory, or via the executable objects created by the
\texttt{install} utility (see \S\ref{sec:tool-install}). Just doing a plain
copy of the \texttt{bin} files will not work!
@@ -95,11 +95,10 @@
\end{enumerate}
Note that settings files are actually full GNU bash scripts. So one may use
-complex shell commands, such as \texttt{if} or \texttt{case} statements, to
-set variables depending on the system architecture or other environment
-variables. Such advanced features should be added only with great care,
-though. In particular, external environment references should be kept at a
-minimum.
+complex shell commands, such as \texttt{if} or \texttt{case} statements to set
+variables depending on the system architecture or other environment variables.
+Such advanced features should be added only with great care, though. In
+particular, external environment references should be kept at a minimum.
\medskip A few variables are somewhat special:
\begin{itemize}
@@ -108,7 +107,7 @@
\texttt{isatool} executables, respectively.
\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have the {\ML}
- system identifier (according to \texttt{ML_IDENTIFIER} automatically
+ system identifier (according to \texttt{ML_IDENTIFIER}) automatically
appended to their values.
\end{itemize}
@@ -224,8 +223,8 @@
-w reset write permissions on OUTPUT
INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
- These are either names to be searched in the Isabelle path, or actual
- file names (containing at least one /).
+ These are either names to be searched in the Isabelle path, or
+ actual file names (containing at least one /).
If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
\end{ttbox}
Input files without path specifications are looked up in the
@@ -361,8 +360,8 @@
\item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus
\texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
-\item \texttt{xterm} refers to a simple xterm based interface which is part of
- the Isabelle distribution.
+\item \texttt{xterm} refers to a simple \textsl{xterm} based interface which
+ is part of the Isabelle distribution.
\item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user
interface!Isamode} for emacs. Isabelle just provides a wrapper for this,
--- a/doc-src/System/misc.tex Mon Oct 18 19:43:18 1999 +0200
+++ b/doc-src/System/misc.tex Tue Oct 19 13:45:51 1999 +0200
@@ -34,8 +34,8 @@
Recursively find .ML files, expand shorthand goal commands. Also
contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
- forward_tac, rewrite_goals_tac on 1-element lists; furthermore expands
- tabs, which are forbidden in SML string constants.
+ forward_tac, rewrite_goals_tac on 1-element lists; furthermore
+ expands tabs, which are forbidden in SML string constants.
Renames old versions of files by appending "~~".
\end{ttbox}
@@ -121,7 +121,8 @@
Usage: install [OPTIONS]
Options are:
- -d DISTDIR use DISTDIR as Isabelle distribution (default ISABELLE_HOME)
+ -d DISTDIR use DISTDIR as Isabelle distribution
+ (default ISABELLE_HOME)
-k install KDE application icon on Desktop
-p DIR install standalone binaries in DIR
@@ -208,7 +209,6 @@
The arguments \texttt{ARGS} are just passed verbatim to each
\texttt{make} invocation.
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
--- a/doc-src/System/present.tex Mon Oct 18 19:43:18 1999 +0200
+++ b/doc-src/System/present.tex Tue Oct 19 13:45:51 1999 +0200
@@ -324,7 +324,7 @@
-\section{Managing logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
+\section{Managing Isabelle logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
The \tooldx{usedir} utility builds object-logic images, or runs example
sessions based on existing logics. Its usage is:
@@ -332,7 +332,6 @@
Usage: usedir LOGIC NAME
Options are:
- -B build mode with THIS_IS_ISABELLE_BUILD indication
-P PATH set path for remote theory browsing information
-b build mode (output heap image, using current dir)
-d FORMAT build document as FORMAT (default false)
@@ -364,11 +363,7 @@
image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command
line. This will be a batch session, running \texttt{ROOT.ML} from the current
directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all
-{\ML} commands required to build the logic. The \texttt{-B} option is like
-\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the
-process environment. This usually causes the \texttt{ISABELLE\_OUTPUT} and
-\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the
-Isabelle distribution directory, rather than the user's home directory.
+{\ML} commands required to build the logic.
In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}
and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}.
@@ -405,7 +400,6 @@
object-logics as a model for your own developments. For example, see
\texttt{src/FOL/IsaMakefile}.
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"