--- a/doc-src/System/basics.tex Mon Jan 12 13:48:40 1998 +0100
+++ b/doc-src/System/basics.tex Mon Jan 12 15:47:43 1998 +0100
@@ -49,9 +49,8 @@
Isabelle employs a somewhat more sophisticated scheme of
\emph{settings files} --- one for site-wide defaults, another for
optional user-specific modifications. With all configuration
-variables in just a few places, this is considered much more
-maintainable and user-friendly than ordinary shell environment
-variables.
+variables in just a few places, this is much more maintainable and
+user-friendly than ordinary shell environment variables.
In particular, we avoid the typical situation where prospective users
of a software package are told to put this and that in their shell
@@ -121,7 +120,7 @@
\end{itemize}
\medskip The Isabelle settings scheme is basically quite simple, but
-non-trivial. For debugging purposes, the generated environment may be
+non-trivial. For debugging purposes, the resulting environment may be
inspected with the \texttt{getenv} utility, see
\S\ref{sec:tool-getenv}.
@@ -171,7 +170,8 @@
\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory
browser information (HTML and graph data) is stored (see also
- \S\ref{sec:info}).
+ \S\ref{sec:info}). The default value is
+ \texttt{\$ISABELLE_HOME_USER/browser_info}.
\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
none is given explicitely by the user --- e.g.\ when running
@@ -201,8 +201,7 @@
\item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any
\texttt{isabelle} session derives an individual directory for
- temporary files. The default is somewhere in \texttt{/tmp}; this
- should not need to be changed under normal circumstances.
+ temporary files. The default is somewhere in \texttt{/tmp}.
\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
actual user interface that the capital \texttt{Isabelle} should
@@ -250,7 +249,7 @@
read-only. That is, the {\ML} world cannot be committed back into the
logic image. Otherwise, a writable session enables commits into
either the input file, or into an alternative output heap file (in
-case this is given as the second argument).
+case this is given as the second argument on the command line).
The read-write state of sessions is determined at startup only, it
cannot be changed intermediately. Also note that heap images may
@@ -258,17 +257,17 @@
themselves to dispose their heap files when they are no longer needed.
\medskip The \texttt{-w} option makes the output heap file read-only
-after terminating the Isabelle session. Thus subsequent invocations
-cause logic image to be read-only automatically.
+after terminating. Thus subsequent invocations cause the logic image
+to be read-only automatically.
\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
passed to the Isabelle session from the command line. Multiple
\texttt{-e}'s are evaluated in order. Strange things may happen when
-errorneous {\ML} code is given. Also make sure that commands are
-terminated properly by semicolon.
+errorneous {\ML} code is given. Also make sure that the {\ML} commands
+are terminated properly by semicolon.
\medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
-\texttt{use"ROOT.ML";} to the {\ML} session.
+``\texttt{use"ROOT.ML";}'' to the {\ML} session.
\medskip The \texttt{-m} option adds identifiers of print modes to be
made active for this session. Typically, this is used by some user
@@ -339,7 +338,7 @@
\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.
+add the tool directories to your shell's search path.
\medskip See chapter~\ref{ch:tools} for descriptions of most utilities
--- a/doc-src/System/fonts.tex Mon Jan 12 13:48:40 1998 +0100
+++ b/doc-src/System/fonts.tex Mon Jan 12 15:47:43 1998 +0100
@@ -1,5 +1,5 @@
-$Id$
+%$Id$
\chapter{Fonts and character encodings}
@@ -14,15 +14,15 @@
\S\ref{sec:interface}) usually do this already by default.
\medskip Displaying non-standard characters requires special screen
-fonts, of course. The \texttt{installfonts} utility takes care of
-this, see \S\ref{sec:tool-installfonts}. Furthermore, some {\ML}
-systems disallow non-\textsc{ascii} characters in literal string
-constants. This problem is avoided by appropriate input filtering
-(see \S\ref{sec:tool-symbolinput}).
+fonts, of course. The \texttt{installfonts} utility takes care of this
+(see \S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems
+disallow non-\textsc{ascii} characters in literal string constants.
+This problem is avoided by appropriate input filtering (see
+\S\ref{sec:tool-symbolinput}).
-These things are usually taken care of automatically behind the
-scenes. Users normally do not have to read the explanations below,
-unless something fails to work.
+These things usually happen behind the scenes. Users normally do not
+have to read the explanations below, unless something really fails to
+work.
\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
@@ -53,6 +53,7 @@
by being told about the Isabelle fonts directory as follows:
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
+
\end{ttbox}
The same also works for remote X11 sessions in a somewhat homogeneous
network, where any X11 display machine also mounts the Isabelle
@@ -63,8 +64,8 @@
is a full workstation with its own file system, you could in principle
just copy the fonts there and do an appropriate \texttt{xset~fp+}
manually before running the Isabelle interface. This is very awkward,
-of course. It is even \emph{impossible} for proper X11 terminals that
-do not have their own file system.
+of course. It is even impossible for proper X11 terminals that do not
+have their own file system.
A much better solution is to have a \emph{font server} offer the
Isabelle fonts to any X11 display on the network. There are already
@@ -89,6 +90,7 @@
\section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
+\label{sec:tool-nonascii}
The \tooldx{nonascii} utility checks files for non-\textsc{ascii}
characters:
@@ -98,10 +100,8 @@
Recursively find .thy/.ML files and check for non-\textsc{ascii}
characters.
\end{ttbox}
-Note that under normal circumstances, non-\textsc{ascii} characters
-should not appear in theories or proof scripts. In particular,
-unexpected problems may happen in conjunction with the Isabelle symbol
-font.
+Under normal circumstances, non-\textsc{ascii} characters do not
+appear in theories and proof scripts.
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
@@ -112,7 +112,7 @@
range 32--127 as part of literal string constants. In order to
circumvent such restrictions, Isabelle employs a general notation
where glyphs are referred by some symbolic name instead of their
-actual encoding: Its general form is \verb|\<|$charname$\verb|>|.
+actual encoding: The general form is \verb|\<|$charname$\verb|>|.
The \tooldx{symbolinput} utility converts a input stream encoded
according to the standard Isabelle font layout into pure
@@ -126,12 +126,10 @@
syntax.
\medskip In many cases, it might be wise not to rely on symbolic
-characters and avoid non-\textsc{ascii} text in files altogether. Then
-symbolic syntax would be really optional, with always suitable
-\textsc{ascii} representations available: In theory definitions,
-symbols appear only in mixfix annotations --- using the
-\verb|\<|$charname$\verb|>| form, proof scripts are just left in plain
-\textsc{ascii}.
-
-Thus users with \textsc{ascii}-only facilities will still be able to
-read your files.
+characters and avoid non-\textsc{ascii} text in files altogether (see
+also \S\ref{sec:tool-nonascii}). Then symbolic syntax would be really
+optional, with always suitable \textsc{ascii} representations
+available: In theory definitions, symbols appear only in mixfix
+annotations --- using the \verb|\<|$charname$\verb|>| form, proof
+scripts are just left in plain \textsc{ascii}. Thus users with
+\textsc{ascii}-only facilities will still be able to read your files.
--- a/doc-src/System/misc.tex Mon Jan 12 13:48:40 1998 +0100
+++ b/doc-src/System/misc.tex Mon Jan 12 15:47:43 1998 +0100
@@ -82,8 +82,8 @@
environment that Isabelle related programs are run in. This usually
contains much more variables than are actually Isabelle settings.
Normally, output is a list of lines of the form
-\mbox{$varname$\texttt{=}$value$}. The \texttt{-b} option causes only
-the values to be printed.
+\mbox{$name$\texttt{=}$value$}. The \texttt{-b} option causes only the
+values to be printed.
\subsection*{Examples}
@@ -102,9 +102,9 @@
isatool getenv -b ISABELLE_PATH
{\out /home/me/isabelle/heaps/smlnj-110:/usr/local/isabelle/heaps/smlnj-110}
\end{ttbox}
-We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=}
-prefix. The value above is what became of the following assignment in
-the default settings file:
+Here we have used the \texttt{-b} option to suppress the
+\texttt{ISABELLE_PATH=} prefix. The value above is what became of the
+following assignment in the default settings file:
\begin{ttbox}
ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
\end{ttbox}
@@ -132,27 +132,29 @@
\medskip The basic \texttt{IsaMakefile} convention is that the default
target builds the actual logic, including its parents if appropriate.
-The \texttt{images} target is intended to build all logic images,
-while the \texttt{test} target shall build all related examples. The
-\texttt{all} target shall build the images and run the examples.
+The \texttt{images} target is intended to build all local logic
+images, while the \texttt{test} target shall build all related
+examples. The \texttt{all} target shall do \texttt{images} and
+\texttt{test}.
\subsection*{Examples}
Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
-object-logics as a model for your own developements.
+object-logics as a model for your own developements. For example, see
+\texttt{src/FOL/IsaMakefile}.
\section{Make all logics -- \texttt{isatool makeall}}
The \tooldx{makeall} utility applies Isabelle make to all logic
-directories of the Isabelle distribution:
+directories of the distribution:
\begin{ttbox}
Usage: makeall [ARGS ...]
Apply isatool make to all logics (passing ARGS).
\end{ttbox}
-The arguments \texttt{ARGS} are just passed verbatim to any
+The arguments \texttt{ARGS} are just passed verbatim to each
\texttt{make} invocation.
@@ -173,7 +175,7 @@
information (HTML etc.) according to settings.
\end{ttbox}
-The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
+Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
\ttindex{IsaMakefile}s of all object-logics distributed with Isabelle
just invoke \texttt{usedir} for the real work, one may control
@@ -195,22 +197,21 @@
assumed that \texttt{ROOT.ML} contains all {\ML} commands required to
build the logic.
-In example mode, on the other hand, \texttt{usedir} runs a read-only
+In example mode on the other hand, \texttt{usedir} runs a read-only
session of \texttt{LOGIC} (typically just built before) and
automatically runs \texttt{ROOT.ML} from within directory
-\texttt{NAME}. I.e.\ it assumes that some file \texttt{ROOT.ML} in
-directory \texttt{NAME} contains appropriate {\ML} commands to run the
-desired examples.
+\texttt{NAME}. It assumes that file \texttt{ROOT.ML} in directory
+\texttt{NAME} contains appropriate {\ML} commands to run the desired
+examples.
\medskip The \texttt{-i} option controls theory browsing data
generation. It may be explicitely turned on or off --- the last
-occurrence of some \texttt{-i} on the command line wins.
+occurrence of \texttt{-i} on the command line wins.
\medskip Any \texttt{usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
-on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which refers
-to the examples of {\ZF} set theory, built upon {\FOL}, built upon
-{\Pure}.
+on others. For example, consider \texttt{Pure/FOL/ex}, which refers to
+the examples of {\FOL} which is built upon {\Pure}.
The current session's identifier is by default just the base name of
the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME}
@@ -221,4 +222,6 @@
\subsection*{Examples}
Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
-object-logics as a model for your own developements.
+object-logics as a model for your own developements. For example, see
+\texttt{src/FOL/IsaMakefile}.
+
--- a/doc-src/System/present.tex Mon Jan 12 13:48:40 1998 +0100
+++ b/doc-src/System/present.tex Mon Jan 12 15:47:43 1998 +0100
@@ -19,7 +19,7 @@
linked with other indexes to represent the hierarchic structure of
Isabelle's logics.
-In addition to the HTML files, Isabelle also generates \texttt{graph}
+In addition to the HTML files, Isabelle also generates \emph{graph}
files that represent the theory hierarchy of a logic. These graphs
can be comfortably displayed by a graph browser Java applet embedded
in the generated HTML pages. There is also a stand-alone version of
@@ -33,13 +33,13 @@
part of the Isabelle distribution, simply append ``\texttt{-i true}''
to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.
For example, to generate browsing information for {\FOL}, first add
-something like this to your private Isabelle settings file:
+something like this to your Isabelle settings file:
\begin{ttbox}
ISABELLE_USEDIR_OPTIONS="-i true"
\end{ttbox}
Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle
-distribution and do an \texttt{isatool make} (or even \texttt{isatool
- make test}).
+distribution and do \texttt{isatool make} (or even \texttt{isatool
+ make all}).
\medskip The directory in which to store theory browsing information
is determined by the \settdx{ISABELLE_BROWSER_INFO} setting.
@@ -58,7 +58,7 @@
\begin{ttbox}
http://www4.informatik.tu-muenchen.de/~isabelle/library/
\end{ttbox}
-Note that this is not necessarily consistent with your local sources!
+Of course, this is not necessarily consistent with your local version!
To present your own theories on the WWW, simply copy the whole
\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server.
@@ -222,7 +222,7 @@
\subsubsection*{The ``File'' menu}
-Please note that, due to Java security restrictions, this menu is not
+Please note that due to Java security restrictions this menu is not
available in the applet version. The meaning of the menu items is as
follows:
\begin{description}
--- a/doc-src/System/system.ind Mon Jan 12 13:48:40 1998 +0100
+++ b/doc-src/System/system.ind Mon Jan 12 15:47:43 1998 +0100
@@ -1,6 +1,6 @@
\begin{theindex}
- \item {\tt browser} tool, 19
+ \item {\tt browser} tool, 18
\indexspace
@@ -26,23 +26,23 @@
\indexspace
\item {\tt INSTALL}, 1
- \item {\tt installfonts} tool, 14
+ \item {\tt installfonts} tool, 13
\item {\tt ISABELLE} setting, 3
\item {\tt Isabelle}, 1, 7
\item {\tt isabelle}, 1, 4
- \item {\tt ISABELLE_BROWSER_INFO} setting, 4, 17
+ \item {\tt ISABELLE_BROWSER_INFO} setting, 4, 16
\item {\tt ISABELLE_DOCS} setting, 4
\item {\tt ISABELLE_HOME} setting, 2, 3
\item {\tt ISABELLE_HOME_USER} setting, 3
\item {\tt ISABELLE_INSTALL_FONTS} setting, 4
- \item {\tt ISABELLE_INSTALLFONTS} setting, 14
+ \item {\tt ISABELLE_INSTALLFONTS} setting, 13
\item {\tt ISABELLE_INTERFACE} setting, 4, 7
\item {\tt ISABELLE_LOGIC} setting, 4
\item {\tt ISABELLE_OUTPUT} setting, 3, 4
\item {\tt ISABELLE_PATH} setting, 3
\item {\tt ISABELLE_TMP_PREFIX} setting, 4
\item {\tt ISABELLE_TOOLS} setting, 4
- \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 11, 17
+ \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 11, 16
\item {\tt IsaMakefile}, 10, 11
\item {\tt ISATOOL} setting, 3
\item {\tt isatool}, 1, 6
@@ -50,29 +50,29 @@
\indexspace
\item {\tt make} tool, 10
- \item {\tt makeall} tool, 10
+ \item {\tt makeall} tool, 11
\item {\tt ML_HOME} setting, 3
\item {\tt ML_OPTIONS} setting, 3
\item {\tt ML_SYSTEM} setting, 3
\indexspace
- \item {\tt nonascii} tool, 15
+ \item {\tt nonascii} tool, 14
\indexspace
\item settings, \bold{1}
- \item {\tt symbolinput} tool, 16
- \item {\tt symbols}, 14
+ \item {\tt symbolinput} tool, 15
+ \item {\tt symbols}, 13
\indexspace
- \item theory browsing information, \bold{17}
- \item theory graph browser, \bold{18}
+ \item theory browsing information, \bold{16}
+ \item theory graph browser, \bold{17}
\indexspace
- \item {\tt use_dir}, 18
+ \item {\tt use_dir}, 17
\item {\tt usedir} tool, 11
\end{theindex}