--- a/doc-src/System/basics.tex Thu Jan 08 18:24:45 1998 +0100
+++ b/doc-src/System/basics.tex Thu Jan 08 18:25:36 1998 +0100
@@ -93,7 +93,7 @@
Thus individual users may override the site-wide defaults. See also
file \texttt{etc/user-settings.sample} in the distribution.
- Typically, user settings should be a few lines only, just containing
+ Typically, a user settings file would contain only a few lines, just
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
@@ -168,6 +168,10 @@
\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
files should be stored by default. The \texttt{ML_SYSTEM} identifier
is appended here, too.
+
+\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory
+ browser information (HTML and graph data) is stored (see also
+ \S\ref{sec:info}).
\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
none is given explicitely by the user --- e.g.\ when running
@@ -195,6 +199,12 @@
display server. X11 fonts are a non-trivial issue, see
\S\ref{sec:tool-installfonts} for more information.
+\item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any
+ \texttt{isabelle} session derives an individual directory for
+ temporary files. The default value of \texttt{ISABELLE_TMP_PREFIX}
+ is \texttt{/tmp/isabelle}; this should not need to be changed under
+ normal circumstances.
+
\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
actual user interface that the capital \texttt{Isabelle} should
invoke. Currently available are \texttt{none}, \texttt{xterm} and
@@ -217,19 +227,21 @@
-m MODE add print mode for output
-q non-interactive session
-r open heap file read-only
+ -u pass 'use"ROOT.ML";' to the ML session
+ -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 (then containing at least one /).
+ 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
\texttt{ISABELLE_PATH} setting, which may consist of multiple
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).
+Likewise, base 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}
@@ -246,12 +258,19 @@
require considerable amounts of disk space. Users are responsible
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.
+
\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.
+\medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
+\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
interface, for example to enable output of mathematical symbols from a
@@ -290,8 +309,6 @@
\begin{ttbox}
isabelle -r Foo
\end{ttbox}
-One may also use something like \texttt{chmod~-w} on the logic image
-to have it read-only automatically.
\medskip The next example demonstrates batch execution of Isabelle. We
print a certain theorem of \texttt{FOL}:
@@ -314,12 +331,13 @@
Available tools are:
+ browser - Isabelle theory graph browser
doc - view Isabelle documentation
- \(\vdots\)
+ \dots
\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
+run within the same settings environment as Isabelle proper, 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.
@@ -341,7 +359,7 @@
\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
+\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.
--- a/doc-src/System/fonts.tex Thu Jan 08 18:24:45 1998 +0100
+++ b/doc-src/System/fonts.tex Thu Jan 08 18:25:36 1998 +0100
@@ -1,10 +1,12 @@
+
+$Id$
\chapter{Fonts and character encodings}
With the advent of print modes 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
+optional input and output of nice mathematical symbols as built-in
option.
Symbolic output is enabled by activating the \ttindex{symbols} print
@@ -14,13 +16,13 @@
\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}).
+systems disallow non-\textsc{ascii} characters in literal string
+constants. This problem is avoided by appropriate input filtering
+(see \S\ref{sec:tool-symbolinput}).
-Both of these are invoked transparently in normal operation. So one
-does not actually have to read the explanations below, unless
-something fails to work.
+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.
\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
@@ -50,22 +52,22 @@
same machine. In this case, most X11 display servers should be happy
by being told about the Isabelle fonts directory as follows:
\begin{ttbox}
-ISABELLE_INSTALLFONTS="xset fp+{\thinspace}$ISABELLE_HOME/lib/fonts; xset fp rehash"
+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 the X11 display machine mounts the Isabelle
-distribution under the same name as the client side.
+network, where any X11 display machine also mounts the Isabelle
+distribution under the \emph{same} name as the client side.
\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.
+of course. It is even \emph{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 X display on the network. There are already
+Isabelle fonts to any X11 display on the network. There are already
suitable servers running at Munich and Cambridge. So in case you have
a sensible Internet connection to either site, you may just attach
yourself as follows:
@@ -80,11 +82,26 @@
\medskip In the unfortunate 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 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.
+setup. The program is called \texttt{xfs} (sometimes just
+\texttt{fs)}, see the \texttt{man} pages of your system. There is an
+example fontserver configuration available in the
+\texttt{lib/fontserver} directory of the Isabelle distribution.
+
+
+\section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
+The \tooldx{nonascii} utility checks files for non-\textsc{ascii}
+characters:
+\begin{ttbox}
+Usage: nonascii [FILES|DIRS...]
+
+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.
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
@@ -111,17 +128,10 @@
\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
+\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.
-
-
-%FIXME not yet
-%\section{ --- \texttt{isatool showsymbols}}
-%
-%\begin{ttbox}
-%\end{ttbox}
--- a/doc-src/System/misc.tex Thu Jan 08 18:24:45 1998 +0100
+++ b/doc-src/System/misc.tex Thu Jan 08 18:25:36 1998 +0100
@@ -22,29 +22,29 @@
\medskip The \texttt{ISABELLE_DOCS} setting specifies the list of
directories (separated by colons) to be scanned for documentations.
-The program for viewing \texttt{dvi} files is set in
-\texttt{DVI_VIEWER}.
+The program for viewing \texttt{dvi} files is determined by the
+\texttt{DVI_VIEWER} setting.
\section{Tuning proof scripts --- \texttt{isatool expandshort}}
The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
-readability a bit:
+readability:
\begin{ttbox}
-Usage: isatool expandshort [FILES ...]
+Usage: expandshort [FILES|DIRS...]
- Expand shorthand goal commands in FILES. Also contracts uses of
- resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
- 1-element lists; furthermore expands tabs, since they are now
- forbidden in ML string constants.
+ Recursively find .ML files, expand shorthand goal commands.
+ Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
+ rewrite_goals_tac on 1-element lists; furthermore expands tabs,
+ since they are now forbidden in ML string constants.
- Renames old versions of FILES by appending "~~".
+ Renames old versions of files by appending "~~".
\end{ttbox}
-In the files supplied as arguments, all occurrences of the shorthand
-commands \texttt{br}, \texttt{be} etc.\ are replaced with the
-corresponding full commands. Shorthand commands should appear one per
-line. The old versions of the files are renamed to have the
-suffix~\verb'~~'.
+In the files or directories supplied as arguments, all occurrences of
+the shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts
+are replaced with the corresponding full commands. The old versions
+of the files are renamed to have the suffix~\verb'~~'.
+
\section{Get logic images --- \texttt{isatool findlogics}}
@@ -81,7 +81,7 @@
With the \texttt{-a} option, one may inspect the full process
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
+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.
@@ -92,15 +92,15 @@
binaries are supposed to reside as follows:
\begin{ttbox}
isatool getenv ML_SYSTEM ML_HOME
-{\out ML_SYSTEM=smlnj-1.09}
-{\out ML_HOME=/usr/local/sml109.27/bin}
+{\out ML_SYSTEM=smlnj-110}
+{\out ML_HOME=/usr/local/smlnj-110/bin}
\end{ttbox}
The next one peeks at the search path that \texttt{isabelle} uses to
locate logic images:
\begin{ttbox}
isatool getenv -b ISABELLE_PATH
-{\out /home/me/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09}
+{\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
@@ -131,9 +131,29 @@
utility, see \S\ref{sec:tool-usedir}.
\medskip The basic \texttt{IsaMakefile} convention is that the default
-target builds the actual logic, including its parents if absent (but
-not if just out of date). Furthermore, the \texttt{test} target shall
-build the logic \emph{and} run it on all distributed examples.
+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.
+
+
+\subsection*{Examples}
+
+Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
+object-logics as a model for your own developements.
+
+
+\section{Make all logics -- \texttt{isatool makeall}}
+
+The \tooldx{makeall} utility applies Isabelle make to all logic
+directories of the Isabelle 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
+\texttt{make} invocation.
\section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir}
@@ -166,20 +186,21 @@
Basically, there are two different modes of operation: \emph{build
mode} (enabled through the \texttt{-b} option) and \emph{example
- mode}.
+ mode} (default).
Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with
input image \texttt{LOGIC} and output to \texttt{NAME}, as provided on
-the command line. 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.
+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.
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.
+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.
\medskip The \texttt{-i} option controls theory browsing data
generation. It may be explicitely turned on or off --- the last
--- a/doc-src/System/present.tex Thu Jan 08 18:24:45 1998 +0100
+++ b/doc-src/System/present.tex Thu Jan 08 18:25:36 1998 +0100
@@ -1,16 +1,17 @@
+
%% $Id$
\chapter{Presenting theories}
\section{Generating theory browsing information} \label{sec:info}
-\index{theory browsing information|bold}
+\index{theory browsing information|bold}
-Isabelle is able to generate theory browsing information, such as HTML documents
-that show a theory's definition, the theorems proved in its ML file and the relationship
-with its ancestors and descendants. HTML is the hypertext markup
-language used on the World Wide Web to represent text containing
-images and links to other documents. These documents may be viewed
-using Web browsers like Netscape or Lynx.
+Isabelle is able to generate theory browsing information, such as HTML
+documents that show a theory's definition, the theorems proved in its
+ML file and the relationship with its ancestors and descendants. HTML
+is the hypertext markup language used on the World Wide Web to
+represent text containing links to other documents. These documents
+may be viewed using Web browsers like Netscape or Lynx.
Besides the three HTML files that are made for every theory
(definition and theorems, ancestors, descendants), Isabelle stores
@@ -18,29 +19,30 @@
linked with other indexes to represent the hierarchic structure of
Isabelle's logics.
-In addition to the HTML files also {\tt *.graph} files representing the theory
-hierarchy graph of a logic are generated. These graphs can be comfortably
-displayed by a graph browser applet embedded in the generated HTML pages. There
-is also a stand-alone version of the graph browser which allows browsing theory
-graphs without having to start a Web browser first. This version also includes
-features such as generating {\sc PostScript} files, which are not available in the
-applet version. The graph browser will be described later in this chapter.
+In addition to the HTML files, Isabelle also generates \texttt{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
+the graph browser which allows browsing theory graphs without having
+to start a Web browser first. This version also includes features such
+as generating {\sc PostScript} files, which are not available in the
+applet version. The graph browser will be described later in this
+chapter.
-\medskip To generate theory browsing information for logics that are 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 \texttt{\~\relax/isabelle/etc/settings} file:
+\medskip To generate theory browsing information for logics that are
+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:
\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}).\\
+ make test}).
-The directory in which to store theory browsing information is determined
-by the \settdx{ISABELLE_BROWSER_INFO} variable in your \texttt{\~\relax/isabelle/etc/settings}
-file.
+\medskip The directory in which to store theory browsing information
+is determined by the \settdx{ISABELLE_BROWSER_INFO} setting.
\medskip As some of Isabelle's logics are based on others (e.g. {\tt
ZF} on {\tt FOL}) and because the HTML files list a theory's
@@ -61,21 +63,23 @@
To present your own theories on the WWW, simply copy the whole
\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server.
+
\section{Extending or adding a logic}
If you add a new subdirectory to Isabelle's logics (or add a
completely new logic), provide a {\tt ROOT.ML} file which reads in the
-theory files. The {\tt ROOT.ML} file will then be processed via the function
+theory files. The {\tt ROOT.ML} file will then be processed via the
+function
\begin{ttbox}\index{*use_dir}
use_dir : string -> unit
\end{ttbox}
-which takes a path as its parameter, changes the working
-directory, executes {\tt ROOT.ML}, and makes sure that theory browsing information
-is generated properly. The {\tt index.html} file written in this directory will
-be automatically linked to the first index found in the (recursively searched)
-super directories.
+which takes a path as its parameter, changes the working directory,
+executes {\tt ROOT.ML}, and makes sure that theory browsing
+information is generated properly. The {\tt index.html} file written
+in this directory will be automatically linked to the first index
+found in the (recursively searched) super directories.
The \texttt{usedir} utility (see also \S\ref{sec:tool-usedir}) will
automatically take care of this.
@@ -91,9 +95,9 @@
section: string -> unit
\end{ttbox}
-in a theory's ML file, which converts a plain string to a HTML
-heading and inserts it before the next theorem proved or stored with
-one of the above functions.
+in a theory's ML file, which converts a plain string to a HTML heading
+and inserts it before the next theorem proved or stored with one of
+the above functions.
%\section*{*Using someone else's database}
@@ -138,103 +142,135 @@
\section{Browsing theory graphs} \label{sec:browse}
\index{theory graph browser|bold}
-The graph browser is a tool for visualizing
-dependency graphs of Isabelle theories. Certain nodes of
-the graph (i.e.~theories) can be grouped together in "directories",
-whose contents may be hidden, thus enabling the user to filter out
-irrelevant information. Because it is written in Java, the browser
-can be used both as a stand-alone application and as an applet.
+The graph browser is a tool for visualizing dependency graphs of
+Isabelle theories. Certain nodes of the graph (i.e.~theories) can be
+grouped together in ``directories'', whose contents may be hidden,
+thus enabling the user to filter out irrelevant information. The
+browser is written in Java, it can be used both as a stand-alone
+application and as an applet.
+
\subsection{Invoking the graph browser}
-The stand-alone version of the browser can be invoked by the command
+
+The stand-alone version of the graph browser is wrapped up as an
+Isabelle tool called \tooldx{browser}:
\begin{ttbox}
-isatool browser [filename]
+Usage: browser [GRAPHFILE]
\end{ttbox}
-When no filename is specified, the browser automatically changes to the directory
-\texttt{ISABELLE_BROWSER_INFO/graph/data}.\\
+When no filename is specified, the browser automatically changes to
+the directory \texttt{ISABELLE_BROWSER_INFO/graph/data}.
-The applet version of the browser can be invoked by opening the {\tt index.html} file
-in the directory \texttt{ISABELLE_BROWSER_INFO} from your Web browser and selecting
-"version for Java capable browsers". Besides, there's a link to the corresponding theory graph
-in every logic's {\tt index.html} file.
+\medskip The applet version of the browser can be invoked by opening
+the {\tt index.html} file in the directory
+\texttt{ISABELLE_BROWSER_INFO} from your Web browser and selecting
+``version for Java capable browsers''. There is also a link to the
+corresponding theory graph in every logic's {\tt index.html} file.
+
\subsection{Using the graph browser}
-The browser's main window, which is shown in figure \ref{browserwindow},
-consists of two subwindows: In the left subwindow, the directory tree
-is displayed. The graph itself is displayed in the right subwindow.
+
+The browser's main window, which is shown in figure
+\ref{browserwindow}, consists of two subwindows: In the left
+subwindow, the directory tree is displayed. The graph itself is
+displayed in the right subwindow.
\begin{figure}[h]
-\setlength{\epsfxsize}{\textwidth}
-\epsffile{browser_screenshot.eps}
-\caption{\label{browserwindow} Browser main window}
+ \includegraphics[width=\textwidth]{browser_screenshot.eps}
+ \caption{\label{browserwindow} Browser main window}
\end{figure}
+
\subsubsection*{The directory tree window}
+
This section describes the usage of the directory browser and the
meaning of the different items in the browser window.
\begin{itemize}
-\item A red arrow before a directory name indicates that the directory is
-currently "folded", i.e.~the nodes in this directory
-are collapsed to one single node. In the right subwindow, the names of
-nodes corresponding to folded directories are enclosed in square brackets
-and displayed in red colour.
-\item A green downward arrow before a directory name indicates that the
-directory is currently "unfolded". It can be folded by clicking on the
-directory name.
-Clicking on the name for a second time unfolds the directory again.
-Alternatively, a directory can also be unfolded by clicking on the
-corresponding node in the right subwindow.
+
+\item A red arrow before a directory name indicates that the directory
+ is currently ``folded'', i.e.~the nodes in this directory are
+ collapsed to one single node. In the right subwindow, the names of
+ nodes corresponding to folded directories are enclosed in square
+ brackets and displayed in red colour.
+
+\item A green downward arrow before a directory name indicates that
+ the directory is currently ``unfolded''. It can be folded by
+ clicking on the directory name. Clicking on the name for a second
+ time unfolds the directory again. Alternatively, a directory can
+ also be unfolded by clicking on the corresponding node in the right
+ subwindow.
+
\item Blue arrows stand before ordinary node (i.e.~theory) names. When
-clicking on such a name, the graph display window focuses to the
-corresponding node. Double clicking invokes a text viewer window in
-which the contents of the theory file are displayed.
+ clicking on such a name, the graph display window focuses to the
+ corresponding node. Double clicking invokes a text viewer window in
+ which the contents of the theory file are displayed.
+
\end{itemize}
+
\subsubsection*{The graph display window}
-When pointing on an ordinary node, an upward and a downward arrow is shown.
-Initially, both of these arrows are coloured green. Clicking on the
+
+When pointing on an ordinary node, an upward and a downward arrow is
+shown. Initially, both of these arrows are green. Clicking on the
upward or downward arrow collapses all predecessor or successor nodes,
respectively. The arrow's colour then changes to red, indicating that
the predecessor or successor nodes are currently collapsed. The node
-corresponding to the collapsed nodes has the name "{\tt [....]}". To
-uncollapse the nodes again, simply click on the red arrow or on the node
-with the name "{\tt [....]}". Similar to the directory browser, the contents
-of theory files can be displayed by double clicking on the corresponding
-node.
+corresponding to the collapsed nodes has the name ``{\tt [....]}''. To
+uncollapse the nodes again, simply click on the red arrow or on the
+node with the name ``{\tt [....]}''. Similar to the directory browser,
+the contents of theory files can be displayed by double clicking on
+the corresponding node.
-\subsubsection*{The "File" menu}
-Please note that, due to security restrictions, this menu is not available
-in the applet version. The meaning of the menu items is as follows:
+
+\subsubsection*{The ``File'' menu}
+
+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}
+
\item[Open$\ldots$] Open a new graph file.
-\item[Export to PostScript] Outputs the current graph in {\sc PostScript}
-format, appropriately scaled to fit on one single sheet of paper.
-The resulting file can be sent directly to a {\sc PostScript} capable printer.
-\item[Export to EPS] Outputs the current graph in Encapsulated {\sc PostScript}
-format. The resulting file can be included in other documents (e.g.~by using
-the \LaTeX \ package "epsf").
+
+\item[Export to PostScript] Outputs the current graph in {\sc
+ PostScript} format, appropriately scaled to fit on one single
+ sheet of paper. The resulting file can printed directly.
+
+\item[Export to EPS] Outputs the current graph in Encapsulated {\sc
+ PostScript} format. The resulting file can be included in other
+ documents.
+
\item[Quit] Quit the graph browser.
+
\end{description}
+
\subsection*{*Syntax of graph definition files}
+
A graph definition file has the following syntax:
\begin{eqnarray*}
-\mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
-vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
-\: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *
+ \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
+ vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
+ \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *
\end{eqnarray*}
+
The meaning of the items in a vertex description is as follows:
\begin{description}
+
\item[vertexname] The name of the vertex.
-\item[vertexID] The vertex identifier. Note that there may be two vertices with equal names,
-whereas identifiers must be unique.
-\item[dirname] The name of the "directory" the vertex should be placed in.
-A "{\tt +}" sign after {\it dirname} indicates that the nodes in the directory
-are initially visible. Directories are initially invisible by default.
-\item[path] The path of the corresponding theory file. This is specified
-relatively to the path of the graph definition file.
-\item[List of successor/predecessor nodes] A "{\tt <}" sign before the list
-means that successor nodes are listed, a "{\tt >}" sign means that predecessor
-nodes are listed. If neither "{\tt <}" nor "{\tt >}" is found, the browser
-assumes that successor nodes are listed.
+
+\item[vertexID] The vertex identifier. Note that there may be two
+ vertices with equal names, whereas identifiers must be unique.
+
+\item[dirname] The name of the ``directory'' the vertex should be
+ placed in. A ``{\tt +}'' sign after {\it dirname} indicates that
+ the nodes in the directory are initially visible. Directories are
+ initially invisible by default.
+
+\item[path] The path of the corresponding theory file. This is
+ specified relatively to the path of the graph definition file.
+
+\item[List of successor/predecessor nodes] A ``{\tt <}'' sign before
+ the list means that successor nodes are listed, a ``{\tt >}'' sign
+ means that predecessor nodes are listed. If neither ``{\tt <}'' nor
+ ``{\tt >}'' is found, the browser assumes that successor nodes are
+ listed.
+
\end{description}
-All names should be put in quotation marks.
--- a/doc-src/System/system.ind Thu Jan 08 18:24:45 1998 +0100
+++ b/doc-src/System/system.ind Thu Jan 08 18:25:36 1998 +0100
@@ -1,5 +1,9 @@
\begin{theindex}
+ \item {\tt browser} tool, 19
+
+ \indexspace
+
\item {\tt doc} tool, 8
\item {\tt DVI_VIEWER} setting, 4
@@ -22,22 +26,23 @@
\indexspace
\item {\tt INSTALL}, 1
- \item {\tt installfonts} tool, 12
+ \item {\tt installfonts} tool, 14
\item {\tt ISABELLE} setting, 3
- \item {\tt Isabelle}, 1, 6
+ \item {\tt Isabelle}, 1, 7
\item {\tt isabelle}, 1, 4
- \item {\tt ISABELLE_BROWSER_INFO} setting, 15
+ \item {\tt ISABELLE_BROWSER_INFO} setting, 4, 17
\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, 12
- \item {\tt ISABELLE_INTERFACE} setting, 4, 6
+ \item {\tt ISABELLE_INSTALLFONTS} setting, 14
+ \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, 15
+ \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 11, 17
\item {\tt IsaMakefile}, 10, 11
\item {\tt ISATOOL} setting, 3
\item {\tt isatool}, 1, 6
@@ -45,24 +50,29 @@
\indexspace
\item {\tt make} tool, 10
+ \item {\tt makeall} tool, 10
\item {\tt ML_HOME} setting, 3
\item {\tt ML_OPTIONS} setting, 3
\item {\tt ML_SYSTEM} setting, 3
\indexspace
+ \item {\tt nonascii} tool, 15
+
+ \indexspace
+
\item settings, \bold{1}
- \item {\tt symbolinput} tool, 13
- \item {\tt symbols}, 12
+ \item {\tt symbolinput} tool, 16
+ \item {\tt symbols}, 14
\indexspace
- \item theory browsing information, \bold{15}
- \item theory graph browser, \bold{16}
+ \item theory browsing information, \bold{17}
+ \item theory graph browser, \bold{18}
\indexspace
- \item {\tt use_dir}, 11, 16
- \item {\tt usedir} tool, 10
+ \item {\tt use_dir}, 18
+ \item {\tt usedir} tool, 11
\end{theindex}
--- a/doc-src/System/system.tex Thu Jan 08 18:24:45 1998 +0100
+++ b/doc-src/System/system.tex Thu Jan 08 18:25:36 1998 +0100
@@ -2,22 +2,18 @@
%% $Id$
\documentclass[12pt]{report}
-\usepackage{a4,epsf}
+\usepackage{a4,graphicx,../iman,../extra}
-\makeatletter
-\input{../iman.sty}
-\input{../extra.sty}
-\makeatother
\title{The Isabelle System Manual}
-\author{{\em Lawrence C. Paulson}\\
- Computer Laboratory \\ University of Cambridge \\
- \texttt{lcp@cl.cam.ac.uk}\\[3ex]
- With Contributions by Tobias Nipkow and Markus Wenzel
- \thanks{Section~\protect\ref{sec:info} was written by Carsten
- Clasohm. Section~\protect\ref{sec:browse} was written by Stefan
- Berghofer. Other parts are by Markus Wenzel.}}
+\author{{\em Lawrence C. Paulson} \\
+ Computer Laboratory \\ University of Cambridge \\
+ \texttt{lcp@cl.cam.ac.uk}\\[3ex]
+ With Contributions by Tobias Nipkow and Markus
+ Wenzel\thanks{Section~\protect\ref{sec:info} was written by Carsten
+ Clasohm. Section~\protect\ref{sec:browse} was written by Stefan
+ Berghofer. Other parts are by Markus Wenzel.}}
\makeindex
@@ -28,22 +24,17 @@
\binperiod %%%treat . like a binary operator
\begin{document}
+
\underscoreoff
\maketitle
\pagenumbering{roman} \tableofcontents \clearfirst
-%\include{introduction}
-
\include{basics}
\include{misc}
\include{fonts}
\include{present}
-%\begingroup
-% \bibliographystyle{plain} \small\raggedright\frenchspacing
-% \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}
-%\endgroup
+\input{system.ind}
-\input{system.ind}
\end{document}