--- a/doc-src/System/basics.tex Tue May 20 19:33:53 1997 +0200
+++ b/doc-src/System/basics.tex Tue May 20 19:34:24 1997 +0200
@@ -3,11 +3,10 @@
\chapter{Basic concepts}
-The \emph{Isabelle System Manual} describes Isabelle together with its
-related tools and user interfaces --- as seen from an outside
-(operating system oriented) view. See the \emph{Isabelle Reference
- Manual} for all internal {\ML} level user commands, on the other
-hand.
+The \emph{Isabelle System Manual} describes Isabelle together with
+related tools and user interfaces as seen from an outside (operating
+system oriented) view. See the \emph{Isabelle Reference Manual} for
+all internal {\ML} level user commands, on the other hand.
\medskip The Isabelle system level environment is based on a few
general concepts:
@@ -31,10 +30,10 @@
\medskip The beginning user would probably just run one of the
interfaces (by invoking the capital \texttt{Isabelle}), and maybe some
-basic other tools like \texttt{doc} (see \S\ref{sec:tool-doc}). This
+basic tools like \texttt{doc} (see \S\ref{sec:tool-doc}). This
assumes that the system has already been installed properly, of
-course.\footnote{In case you have to do this yourself from scratch,
- see the \ttindex{INSTALL} file in the top-level directory of the
+course.\footnote{In case you have to do this yourself, see the
+ \ttindex{INSTALL} file in the top-level directory of the
distribution. The information provided there should be sufficient as
a start.}
@@ -50,7 +49,7 @@
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 only one or two places, this is considered much more
+variables in just a few places, this is considered much more
maintainable and user-friendly than ordinary shell environment
variables.
@@ -64,7 +63,7 @@
\subsection{Building the environment}
-Whenever any of the Isabelle executables is run, theri settings
+Whenever any of the Isabelle executables is run, their settings
environment is built as follows:
\begin{enumerate}
@@ -94,11 +93,11 @@
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 required. One should definitely
- \emph{not} start with a full copy the central
- \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very anoying
- maintainance problems later, when the Isabelle installation is
- updated or changed otherwise.
+ 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.
\end{enumerate}
@@ -166,8 +165,8 @@
automatically.
\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
- files should be stored. The \texttt{ML_SYSTEM} identifier is
- appended here, too.
+ files should be stored by default. The \texttt{ML_SYSTEM} identifier
+ is appended here, too.
\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
none is given explicitely by the user --- e.g.\ when running
@@ -186,14 +185,14 @@
\item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories
with documentation files.
-
-\item[\settdx{DVI_VIEWER}] specifies the program to be used for
+
+\item[\settdx{DVI_VIEWER}] specifies the command to be used for
displaying \texttt{dvi} files.
\item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the
- Isabelle symbol fonts are installed into your running X11 display
- server. X11 fonts are a non-trivial issue, see \S\ref{sec:fonts} for
- more information.
+ Isabelle symbol fonts are installed into your currently running X11
+ display server. X11 fonts are a non-trivial issue, see
+ \S\ref{sec:tool-installfonts} for more information.
\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
actual user interface that the capital \texttt{Isabelle} should
@@ -228,8 +227,8 @@
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
-could also be given by including at least one \texttt{/} in the name
-(use \texttt{./} to refer to the current directory).
+may also be given by including at least one \texttt{/} in the name
+(hint: use \texttt{./} to refer to the current directory).
\subsection*{Options}
@@ -248,16 +247,16 @@
\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 the given order. Strange things may
-happen when errorneous {\ML} code is supplied. Also make sure that
-commands are terminated properly by semicolon.
+\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.
-\medskip The \texttt{-m} option adds identifiers of print modes that
-are 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.
+\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.
\medskip Isabelle normally enters an interactice {\ML} top-level loop
(after processing the \texttt{-e} texts). The \texttt{-q} option
@@ -284,7 +283,7 @@
megabytes!
The \texttt{Foo} session may be continued later (still in writable
-state) at exactly the same point:
+state) by:
\begin{ttbox}
isabelle Foo
\end{ttbox}
--- a/doc-src/System/fonts.tex Tue May 20 19:33:53 1997 +0200
+++ b/doc-src/System/fonts.tex Tue May 20 19:34:24 1997 +0200
@@ -1,20 +1,21 @@
\chapter{Fonts and character encodings}
-With the advent of print modes in Isabelle (see also The
-\emph{Isabelle Reference Manual}, variant forms of output have become
-very easy. As the canonical application of this feature, {\Pure} and
-major object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional output
-(and input) of nice mathematical symbols out of the box.
+With print modes being now available in Isabelle, variant forms of
+output have become very easy. As the canonical application of this
+feature, {\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF)
+support optional input and output of nice mathematical symbols as an
+built-in option.
Symbolic output is enabled by activating the \ttindex{symbols} print
mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
-\S\ref{sec:isa-xterm}) usually do this by default.
+\S\ref{sec:isa-xterm}) usually do this already by default.
-\medskip Of course, this requires special screen fonts (see
-\S\ref{sec:tool-installfonts}). Furthermore, various {\ML} systems
-cause some problems with non-\textsc{ascii} characters in literal
-strings. These are avoided by the \texttt{symbolinput} filter (see
+\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 strings.
+This problem is avoided by the \texttt{symbolinput} filter (see
\S\ref{sec:tool-symbolinput}).
Both of these are invoked transparently in normal operation. So one
@@ -22,7 +23,7 @@
something fails to work.
-\section{Telling X11 about Isabelle fonts --- \texttt{isatool installfonts}}
+\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
\label{sec:tool-installfonts}
The \tooldx{installfonts} utility ensures that your currently running
@@ -35,19 +36,19 @@
(May be safely called repeatedly.)
\end{ttbox}
Note that this need not be called manually under normal circumstances
---- user interfaces depending on the Isabelle fonts will invoke
-\texttt{installfonts} transparently.
+--- user interfaces depending on the Isabelle fonts usually invoke
+\texttt{installfonts} automatically.
\medskip As simple as this might appear to be, it is not! X11 fonts
are a surprisingly complicated matter. Depending on your network
structure, fonts might have to be installed differently. This has to
-be specified via the \settdx{ISABELLE_INSTALLFONTS}.
+be specified via the \settdx{ISABELLE_INSTALLFONTS} variable in your
+local settings.
\medskip In the simplest situation, X11 is used only locally, i.e.\
the client program (Isabelle) and the display server are run on the
-same machine. Then most X11 display servers should be happy to being
-just told about the directory where the fonts reside within the
-Isabelle distribution:
+same machine. In this case, most X11 display servers should be happy
+by being about the directory where the fonts reside as follows:
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
\end{ttbox}
@@ -55,33 +56,64 @@
network, where the X11 display machine mounts the Isabelle
distribution under the same name as the client side.
-\medskip Above method fails, if the display machine does have the font
-files at the same location as the client. In case your server 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 awkward, of course, but
-is even \emph{impossible} for proper X terminals that do not have
-their own file system.
+\medskip Above method fails, though, if the display machine does have
+the font files at the same location as the client. In case your server
+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 X terminals that do
+not have their own file system.
-A much better solution to this problem is to use an \emph{X11 font
- server}, offering the Isabelle font to the Net. In principle it is
-relatively easy to setup one your own --- the program is called
-\texttt{xfs} (or just \texttt{fs)}, see the \texttt{man} pages of your
-system.
-
-Your are very lucky, though, if you have a sensible connection to the
-Internet. We already offer a world-wide X11 font service for the
-Isabelle fonts. To have \texttt{installfonts} make use of this, just
-set \texttt{ISABELLE_INSTALLFONTS} is follows:
+A much better solution to this problem is to have an X11 \emph{font
+ server} offer the Isabelle fonts to any X11 display on the network.
+There is already a font server running at Munich. So in case you have
+a sensible Internet connection, you may plug attach yourself as
+follows:
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
\end{ttbox}
+\medskip In the (rare?) case that neither local fonts work, nor
+accessing our world-wide font service is practical, it might be best
+to start your own in-house font service. This is in principle quite
+easy to setup. The program is called \texttt{xfs} (or just
+\texttt{fs)}, see the \texttt{man} pages of your system. There is an
+example configuration available in the \texttt{lib/fontserver}
+directory of the Isabelle distribution.
+
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
\label{sec:tool-symbolinput}
+Processing non-\textsc{ascii} text is notoriously difficult. Some
+{\ML} systems reject character codes outside the 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
+\texttt{$\backslash$<$charname$>}.
+
+The \tooldx{symbolinput} utility converts a input stream encoded
+according to the standard Isabelle font layout into pure
+\textsc{ascii} text. There is no usage --- \texttt{symbolinput} just
+works from standard input to standard output, without any options
+available.
+
+\medskip For example, the non-\textsc{ascii} input \texttt{"A $\land$
+ B $\lor$ C"} is replaced by \texttt{"A $\backslash\backslash$<and> B
+ $\backslash\backslash$<or> C"}.
+
+\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
+\texttt{ascii} representations available. In theory definitions
+symbols appear only in mixfix annotations --- using the
+\texttt{$\backslash$<$charname$>} form, proof scripts are just left in
+plain \texttt{ascii}.
+
+Thus users with \texttt{ascii}-only facilities will still be able to
+read your files.
+
%FIXME not yet
%\section{ --- \texttt{isatool showsymbols}}
--- a/doc-src/System/misc.tex Tue May 20 19:33:53 1997 +0200
+++ b/doc-src/System/misc.tex Tue May 20 19:34:24 1997 +0200
@@ -31,7 +31,7 @@
The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
readability a bit:
\begin{ttbox}
-Usage: expandshort [FILES ...]
+Usage: isatool expandshort [FILES ...]
Expand shorthand goal commands in FILES. Also contracts uses of
resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
@@ -58,7 +58,7 @@
\end{ttbox}
The base names of all files found on the path are printed --- sorted
and with duplicates removed. Also note that \texttt{ISABELLE_PATH}
-implicitely depends upon \texttt{ML_SYSTEM}. Thus switching to another
+implicitly depends upon \texttt{ML_SYSTEM}. Thus switching to another
{\ML} compiler may change the set of logic images available.
@@ -124,18 +124,19 @@
ARGS are directly passed to the system make program.
\end{ttbox}
Note that the Isabelle settings environment is also active. Thus one
-may refer to its values within the \texttt{IsaMakefile}, e.g.\
+may refer to its values within the \ttindex{IsaMakefile}, e.g.\
\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the
make file also inherit this environment.
-\medskip You may want to have a look at the \texttt{IsaMakefile}s of
-the distributed object-logics as examples for your own developements.
+Typically, \texttt{IsaMakefile}s defer the real work to the
+\texttt{usedir} utility, see \S\ref{sec:tool-usedir}.
+
\section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir}
-FIXME
-
+The \tooldx{usedir} utility builds object-logic images, or runs
+example sessions based on existing logics. Its usage is:
%FIXME
% -g BOOL generate theory graph data (default false)
\begin{ttbox}
@@ -150,4 +151,50 @@
information (HTML etc.) according to settings.
\end{ttbox}
-FIXME
+The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
+implicitely 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
+compilation options globally via above variable. In particular,
+generation of \rmindex{HTML} browsing information is enabled or
+disabled this way.
+
+
+\subsection*{Options}
+
+There are two slightly different modes of operation: \emph{build} mode
+(enabled through the \texttt{-b} option) and \emph{example} mode.
+
+Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with
+input image \texttt{LOGIC} and output to \texttt{NAME}, as provided as
+arguments. This will be a batch session, executing just
+\texttt{use_dir".";}\index{*use_dir}, and then quitting. It is assumed
+that there is a file \texttt{ROOT.ML} in the current directory
+containing all {\ML} commands required to build the logic.
+
+In example mode, on the other hand, \texttt{usedir} runs a read-only
+session of \texttt{LOGIC} (typically just built before) and does an
+automatic \texttt{use_dir"NAME";}. I.e.\ it assumes that some file
+\texttt{ROOT.ML} in directory \texttt{NAME} contains appropriate {\ML}
+commands to run the desired examples.
+
+\medskip The \texttt{-h} option controls HTML browsing data
+generation. It may be explicitely turned on or off --- the last
+occurrence of some \texttt{-h} on the command line wins.
+
+\medskip Any \texttt{usedir} session is named by some \emph{session
+ identifier}. These may accumulate, documenting the way sessions
+depend on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which
+refers the examples of {\ZF} set theory, built upon {\FOL}, built upon
+{\Pure}.
+
+The current session's identifier is by default just the base name of
+the \texttt{LOGIC} argument (in build mode), or the \texttt{NAME}
+argument (in example mode). This may be overridden explicitely via the
+\texttt{-s} option.
+
+
+\subsection*{Examples}
+
+Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
+object-logics as a model for your own developements.
--- a/doc-src/System/system.tex Tue May 20 19:33:53 1997 +0200
+++ b/doc-src/System/system.tex Tue May 20 19:34:24 1997 +0200
@@ -16,7 +16,7 @@
\texttt{lcp@cl.cam.ac.uk}\\[3ex]
With Contributions by Tobias Nipkow and Markus Wenzel%
\thanks{Section~\protect\ref{sec:html} was written by Carsten
- Clasohm. Chapter~\protect\ref{browse} was written by Stefan
+ Clasohm. Chapter~\protect\ref{sec:browse} was written by Stefan
Berghofer. Other parts are by Markus Wenzel.}}
\makeindex