# HG changeset patch # User wenzelm # Date 884616463 -3600 # Node ID 1d7f8faaaea38dc3872866c614deb38d8971f69e # Parent 2c4b3b31a354a398162089a13377f70b7fe4d29d tuned; diff -r 2c4b3b31a354 -r 1d7f8faaaea3 doc-src/System/basics.tex --- 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 diff -r 2c4b3b31a354 -r 1d7f8faaaea3 doc-src/System/fonts.tex --- 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. diff -r 2c4b3b31a354 -r 1d7f8faaaea3 doc-src/System/misc.tex --- 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}. + diff -r 2c4b3b31a354 -r 1d7f8faaaea3 doc-src/System/present.tex --- 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} diff -r 2c4b3b31a354 -r 1d7f8faaaea3 doc-src/System/system.ind --- 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}