tuned;
authorwenzelm
Mon Jan 12 15:47:43 1998 +0100 (1998-01-12)
changeset 45551d7f8faaaea3
parent 4554 2c4b3b31a354
child 4556 e7a4683c0026
tuned;
doc-src/System/basics.tex
doc-src/System/fonts.tex
doc-src/System/misc.tex
doc-src/System/present.tex
doc-src/System/system.ind
     1.1 --- a/doc-src/System/basics.tex	Mon Jan 12 13:48:40 1998 +0100
     1.2 +++ b/doc-src/System/basics.tex	Mon Jan 12 15:47:43 1998 +0100
     1.3 @@ -49,9 +49,8 @@
     1.4  Isabelle employs a somewhat more sophisticated scheme of
     1.5  \emph{settings files} --- one for site-wide defaults, another for
     1.6  optional user-specific modifications.  With all configuration
     1.7 -variables in just a few places, this is considered much more
     1.8 -maintainable and user-friendly than ordinary shell environment
     1.9 -variables.
    1.10 +variables in just a few places, this is much more maintainable and
    1.11 +user-friendly than ordinary shell environment variables.
    1.12  
    1.13  In particular, we avoid the typical situation where prospective users
    1.14  of a software package are told to put this and that in their shell
    1.15 @@ -121,7 +120,7 @@
    1.16  \end{itemize}
    1.17  
    1.18  \medskip The Isabelle settings scheme is basically quite simple, but
    1.19 -non-trivial.  For debugging purposes, the generated environment may be
    1.20 +non-trivial.  For debugging purposes, the resulting environment may be
    1.21  inspected with the \texttt{getenv} utility, see
    1.22  \S\ref{sec:tool-getenv}.
    1.23  
    1.24 @@ -171,7 +170,8 @@
    1.25    
    1.26  \item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory
    1.27    browser information (HTML and graph data) is stored (see also
    1.28 -  \S\ref{sec:info}).
    1.29 +  \S\ref{sec:info}).  The default value is
    1.30 +  \texttt{\$ISABELLE_HOME_USER/browser_info}.
    1.31  
    1.32  \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
    1.33    none is given explicitely by the user --- e.g.\ when running
    1.34 @@ -201,8 +201,7 @@
    1.35    
    1.36  \item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any
    1.37    \texttt{isabelle} session derives an individual directory for
    1.38 -  temporary files.  The default is somewhere in \texttt{/tmp}; this
    1.39 -  should not need to be changed under normal circumstances.
    1.40 +  temporary files.  The default is somewhere in \texttt{/tmp}.
    1.41    
    1.42  \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
    1.43    actual user interface that the capital \texttt{Isabelle} should
    1.44 @@ -250,7 +249,7 @@
    1.45  read-only. That is, the {\ML} world cannot be committed back into the
    1.46  logic image.  Otherwise, a writable session enables commits into
    1.47  either the input file, or into an alternative output heap file (in
    1.48 -case this is given as the second argument).
    1.49 +case this is given as the second argument on the command line).
    1.50  
    1.51  The read-write state of sessions is determined at startup only, it
    1.52  cannot be changed intermediately. Also note that heap images may
    1.53 @@ -258,17 +257,17 @@
    1.54  themselves to dispose their heap files when they are no longer needed.
    1.55  
    1.56  \medskip The \texttt{-w} option makes the output heap file read-only
    1.57 -after terminating the Isabelle session.  Thus subsequent invocations
    1.58 -cause logic image to be read-only automatically.
    1.59 +after terminating.  Thus subsequent invocations cause the logic image
    1.60 +to be read-only automatically.
    1.61  
    1.62  \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
    1.63  passed to the Isabelle session from the command line. Multiple
    1.64  \texttt{-e}'s are evaluated in order. Strange things may happen when
    1.65 -errorneous {\ML} code is given. Also make sure that commands are
    1.66 -terminated properly by semicolon.
    1.67 +errorneous {\ML} code is given. Also make sure that the {\ML} commands
    1.68 +are terminated properly by semicolon.
    1.69  
    1.70  \medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
    1.71 -\texttt{use"ROOT.ML";} to the {\ML} session.
    1.72 +``\texttt{use"ROOT.ML";}'' to the {\ML} session.
    1.73  
    1.74  \medskip The \texttt{-m} option adds identifiers of print modes to be
    1.75  made active for this session. Typically, this is used by some user
    1.76 @@ -339,7 +338,7 @@
    1.77  \S\ref{sec:settings}.  The set of available tools is collected by
    1.78  isatool from the directories listed in the \texttt{ISABELLE_TOOLS}
    1.79  setting.  Do not try to call the scripts directly. Neither should you
    1.80 -add the tools directories to your shell's search path.
    1.81 +add the tool directories to your shell's search path.
    1.82  
    1.83  
    1.84  \medskip See chapter~\ref{ch:tools} for descriptions of most utilities
     2.1 --- a/doc-src/System/fonts.tex	Mon Jan 12 13:48:40 1998 +0100
     2.2 +++ b/doc-src/System/fonts.tex	Mon Jan 12 15:47:43 1998 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  
     2.5 -$Id$
     2.6 +%$Id$
     2.7  
     2.8  \chapter{Fonts and character encodings}
     2.9  
    2.10 @@ -14,15 +14,15 @@
    2.11  \S\ref{sec:interface}) usually do this already by default.
    2.12  
    2.13  \medskip Displaying non-standard characters requires special screen
    2.14 -fonts, of course. The \texttt{installfonts} utility takes care of
    2.15 -this, see \S\ref{sec:tool-installfonts}. Furthermore, some {\ML}
    2.16 -systems disallow non-\textsc{ascii} characters in literal string
    2.17 -constants.  This problem is avoided by appropriate input filtering
    2.18 -(see \S\ref{sec:tool-symbolinput}).
    2.19 +fonts, of course. The \texttt{installfonts} utility takes care of this
    2.20 +(see \S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems
    2.21 +disallow non-\textsc{ascii} characters in literal string constants.
    2.22 +This problem is avoided by appropriate input filtering (see
    2.23 +\S\ref{sec:tool-symbolinput}).
    2.24  
    2.25 -These things are usually taken care of automatically behind the
    2.26 -scenes.  Users normally do not have to read the explanations below,
    2.27 -unless something fails to work.
    2.28 +These things usually happen behind the scenes.  Users normally do not
    2.29 +have to read the explanations below, unless something really fails to
    2.30 +work.
    2.31  
    2.32  
    2.33  \section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
    2.34 @@ -53,6 +53,7 @@
    2.35  by being told about the Isabelle fonts directory as follows:
    2.36  \begin{ttbox}
    2.37  ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
    2.38 +
    2.39  \end{ttbox}
    2.40  The same also works for remote X11 sessions in a somewhat homogeneous
    2.41  network, where any X11 display machine also mounts the Isabelle
    2.42 @@ -63,8 +64,8 @@
    2.43  is a full workstation with its own file system, you could in principle
    2.44  just copy the fonts there and do an appropriate \texttt{xset~fp+}
    2.45  manually before running the Isabelle interface. This is very awkward,
    2.46 -of course. It is even \emph{impossible} for proper X11 terminals that
    2.47 -do not have their own file system.
    2.48 +of course. It is even impossible for proper X11 terminals that do not
    2.49 +have their own file system.
    2.50  
    2.51  A much better solution is to have a \emph{font server} offer the
    2.52  Isabelle fonts to any X11 display on the network.  There are already
    2.53 @@ -89,6 +90,7 @@
    2.54  
    2.55  
    2.56  \section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
    2.57 +\label{sec:tool-nonascii}
    2.58  
    2.59  The \tooldx{nonascii} utility checks files for non-\textsc{ascii}
    2.60  characters:
    2.61 @@ -98,10 +100,8 @@
    2.62  Recursively find .thy/.ML files and check for non-\textsc{ascii}
    2.63  characters.
    2.64  \end{ttbox}
    2.65 -Note that under normal circumstances, non-\textsc{ascii} characters
    2.66 -should not appear in theories or proof scripts.  In particular,
    2.67 -unexpected problems may happen in conjunction with the Isabelle symbol
    2.68 -font.
    2.69 +Under normal circumstances, non-\textsc{ascii} characters do not
    2.70 +appear in theories and proof scripts.
    2.71  
    2.72  
    2.73  \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
    2.74 @@ -112,7 +112,7 @@
    2.75  range 32--127 as part of literal string constants. In order to
    2.76  circumvent such restrictions, Isabelle employs a general notation
    2.77  where glyphs are referred by some symbolic name instead of their
    2.78 -actual encoding: Its general form is \verb|\<|$charname$\verb|>|.
    2.79 +actual encoding: The general form is \verb|\<|$charname$\verb|>|.
    2.80  
    2.81  The \tooldx{symbolinput} utility converts a input stream encoded
    2.82  according to the standard Isabelle font layout into pure
    2.83 @@ -126,12 +126,10 @@
    2.84  syntax.
    2.85  
    2.86  \medskip In many cases, it might be wise not to rely on symbolic
    2.87 -characters and avoid non-\textsc{ascii} text in files altogether. Then
    2.88 -symbolic syntax would be really optional, with always suitable
    2.89 -\textsc{ascii} representations available: In theory definitions,
    2.90 -symbols appear only in mixfix annotations --- using the
    2.91 -\verb|\<|$charname$\verb|>| form, proof scripts are just left in plain
    2.92 -\textsc{ascii}.
    2.93 -
    2.94 -Thus users with \textsc{ascii}-only facilities will still be able to
    2.95 -read your files.
    2.96 +characters and avoid non-\textsc{ascii} text in files altogether (see
    2.97 +also \S\ref{sec:tool-nonascii}). Then symbolic syntax would be really
    2.98 +optional, with always suitable \textsc{ascii} representations
    2.99 +available: In theory definitions, symbols appear only in mixfix
   2.100 +annotations --- using the \verb|\<|$charname$\verb|>| form, proof
   2.101 +scripts are just left in plain \textsc{ascii}.  Thus users with
   2.102 +\textsc{ascii}-only facilities will still be able to read your files.
     3.1 --- a/doc-src/System/misc.tex	Mon Jan 12 13:48:40 1998 +0100
     3.2 +++ b/doc-src/System/misc.tex	Mon Jan 12 15:47:43 1998 +0100
     3.3 @@ -82,8 +82,8 @@
     3.4  environment that Isabelle related programs are run in. This usually
     3.5  contains much more variables than are actually Isabelle settings.
     3.6  Normally, output is a list of lines of the form
     3.7 -\mbox{$varname$\texttt{=}$value$}. The \texttt{-b} option causes only
     3.8 -the values to be printed.
     3.9 +\mbox{$name$\texttt{=}$value$}. The \texttt{-b} option causes only the
    3.10 +values to be printed.
    3.11  
    3.12  
    3.13  \subsection*{Examples}
    3.14 @@ -102,9 +102,9 @@
    3.15  isatool getenv -b ISABELLE_PATH
    3.16  {\out /home/me/isabelle/heaps/smlnj-110:/usr/local/isabelle/heaps/smlnj-110}
    3.17  \end{ttbox}
    3.18 -We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=}
    3.19 -prefix.  The value above is what became of the following assignment in
    3.20 -the default settings file:
    3.21 +Here we have used the \texttt{-b} option to suppress the
    3.22 +\texttt{ISABELLE_PATH=} prefix.  The value above is what became of the
    3.23 +following assignment in the default settings file:
    3.24  \begin{ttbox}
    3.25  ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
    3.26  \end{ttbox}
    3.27 @@ -132,27 +132,29 @@
    3.28  
    3.29  \medskip The basic \texttt{IsaMakefile} convention is that the default
    3.30  target builds the actual logic, including its parents if appropriate.
    3.31 -The \texttt{images} target is intended to build all logic images,
    3.32 -while the \texttt{test} target shall build all related examples.  The
    3.33 -\texttt{all} target shall build the images and run the examples.
    3.34 +The \texttt{images} target is intended to build all local logic
    3.35 +images, while the \texttt{test} target shall build all related
    3.36 +examples.  The \texttt{all} target shall do \texttt{images} and
    3.37 +\texttt{test}.
    3.38  
    3.39  
    3.40  \subsection*{Examples}
    3.41  
    3.42  Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
    3.43 -object-logics as a model for your own developements.
    3.44 +object-logics as a model for your own developements.  For example, see
    3.45 +\texttt{src/FOL/IsaMakefile}.
    3.46  
    3.47  
    3.48  \section{Make all logics -- \texttt{isatool makeall}}
    3.49  
    3.50  The \tooldx{makeall} utility applies Isabelle make to all logic
    3.51 -directories of the Isabelle distribution:
    3.52 +directories of the distribution:
    3.53  \begin{ttbox}
    3.54  Usage: makeall [ARGS ...]
    3.55  
    3.56    Apply isatool make to all logics (passing ARGS).
    3.57  \end{ttbox}
    3.58 -The arguments \texttt{ARGS} are just passed verbatim to any
    3.59 +The arguments \texttt{ARGS} are just passed verbatim to each
    3.60  \texttt{make} invocation.
    3.61  
    3.62  
    3.63 @@ -173,7 +175,7 @@
    3.64    information (HTML etc.) according to settings.
    3.65  \end{ttbox}
    3.66  
    3.67 -The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
    3.68 +Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
    3.69  implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
    3.70  \ttindex{IsaMakefile}s of all object-logics distributed with Isabelle
    3.71  just invoke \texttt{usedir} for the real work, one may control
    3.72 @@ -195,22 +197,21 @@
    3.73  assumed that \texttt{ROOT.ML} contains all {\ML} commands required to
    3.74  build the logic.
    3.75  
    3.76 -In example mode, on the other hand, \texttt{usedir} runs a read-only
    3.77 +In example mode on the other hand, \texttt{usedir} runs a read-only
    3.78  session of \texttt{LOGIC} (typically just built before) and
    3.79  automatically runs \texttt{ROOT.ML} from within directory
    3.80 -\texttt{NAME}.  I.e.\ it assumes that some file \texttt{ROOT.ML} in
    3.81 -directory \texttt{NAME} contains appropriate {\ML} commands to run the
    3.82 -desired examples.
    3.83 +\texttt{NAME}.  It assumes that file \texttt{ROOT.ML} in directory
    3.84 +\texttt{NAME} contains appropriate {\ML} commands to run the desired
    3.85 +examples.
    3.86  
    3.87  \medskip The \texttt{-i} option controls theory browsing data
    3.88  generation. It may be explicitely turned on or off --- the last
    3.89 -occurrence of some \texttt{-i} on the command line wins.
    3.90 +occurrence of \texttt{-i} on the command line wins.
    3.91  
    3.92  \medskip Any \texttt{usedir} session is named by some \emph{session
    3.93    identifier}. These accumulate, documenting the way sessions depend
    3.94 -on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which refers
    3.95 -to the examples of {\ZF} set theory, built upon {\FOL}, built upon
    3.96 -{\Pure}.
    3.97 +on others. For example, consider \texttt{Pure/FOL/ex}, which refers to
    3.98 +the examples of {\FOL} which is built upon {\Pure}.
    3.99  
   3.100  The current session's identifier is by default just the base name of
   3.101  the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME}
   3.102 @@ -221,4 +222,6 @@
   3.103  \subsection*{Examples}
   3.104  
   3.105  Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
   3.106 -object-logics as a model for your own developements.
   3.107 +object-logics as a model for your own developements.  For example, see
   3.108 +\texttt{src/FOL/IsaMakefile}.
   3.109 +
     4.1 --- a/doc-src/System/present.tex	Mon Jan 12 13:48:40 1998 +0100
     4.2 +++ b/doc-src/System/present.tex	Mon Jan 12 15:47:43 1998 +0100
     4.3 @@ -19,7 +19,7 @@
     4.4  linked with other indexes to represent the hierarchic structure of
     4.5  Isabelle's logics.
     4.6  
     4.7 -In addition to the HTML files, Isabelle also generates \texttt{graph}
     4.8 +In addition to the HTML files, Isabelle also generates \emph{graph}
     4.9  files that represent the theory hierarchy of a logic.  These graphs
    4.10  can be comfortably displayed by a graph browser Java applet embedded
    4.11  in the generated HTML pages. There is also a stand-alone version of
    4.12 @@ -33,13 +33,13 @@
    4.13  part of the Isabelle distribution, simply append ``\texttt{-i true}''
    4.14  to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.
    4.15  For example, to generate browsing information for {\FOL}, first add
    4.16 -something like this to your private Isabelle settings file:
    4.17 +something like this to your Isabelle settings file:
    4.18  \begin{ttbox}
    4.19  ISABELLE_USEDIR_OPTIONS="-i true"
    4.20  \end{ttbox}
    4.21  Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle
    4.22 -distribution and do an \texttt{isatool make} (or even \texttt{isatool
    4.23 -  make test}).
    4.24 +distribution and do \texttt{isatool make} (or even \texttt{isatool
    4.25 +  make all}).
    4.26  
    4.27  \medskip The directory in which to store theory browsing information
    4.28  is determined by the \settdx{ISABELLE_BROWSER_INFO} setting.
    4.29 @@ -58,7 +58,7 @@
    4.30  \begin{ttbox}
    4.31  http://www4.informatik.tu-muenchen.de/~isabelle/library/
    4.32  \end{ttbox}
    4.33 -Note that this is not necessarily consistent with your local sources!
    4.34 +Of course, this is not necessarily consistent with your local version!
    4.35  
    4.36  To present your own theories on the WWW, simply copy the whole
    4.37  \texttt{ISABELLE_BROWSER_INFO} directory to your WWW server.
    4.38 @@ -222,7 +222,7 @@
    4.39  
    4.40  \subsubsection*{The ``File'' menu}
    4.41  
    4.42 -Please note that, due to Java security restrictions, this menu is not
    4.43 +Please note that due to Java security restrictions this menu is not
    4.44  available in the applet version. The meaning of the menu items is as
    4.45  follows:
    4.46  \begin{description}
     5.1 --- a/doc-src/System/system.ind	Mon Jan 12 13:48:40 1998 +0100
     5.2 +++ b/doc-src/System/system.ind	Mon Jan 12 15:47:43 1998 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4  \begin{theindex}
     5.5  
     5.6 -  \item {\tt browser} tool, 19
     5.7 +  \item {\tt browser} tool, 18
     5.8  
     5.9    \indexspace
    5.10  
    5.11 @@ -26,23 +26,23 @@
    5.12    \indexspace
    5.13  
    5.14    \item {\tt INSTALL}, 1
    5.15 -  \item {\tt installfonts} tool, 14
    5.16 +  \item {\tt installfonts} tool, 13
    5.17    \item {\tt ISABELLE} setting, 3
    5.18    \item {\tt Isabelle}, 1, 7
    5.19    \item {\tt isabelle}, 1, 4
    5.20 -  \item {\tt ISABELLE_BROWSER_INFO} setting, 4, 17
    5.21 +  \item {\tt ISABELLE_BROWSER_INFO} setting, 4, 16
    5.22    \item {\tt ISABELLE_DOCS} setting, 4
    5.23    \item {\tt ISABELLE_HOME} setting, 2, 3
    5.24    \item {\tt ISABELLE_HOME_USER} setting, 3
    5.25    \item {\tt ISABELLE_INSTALL_FONTS} setting, 4
    5.26 -  \item {\tt ISABELLE_INSTALLFONTS} setting, 14
    5.27 +  \item {\tt ISABELLE_INSTALLFONTS} setting, 13
    5.28    \item {\tt ISABELLE_INTERFACE} setting, 4, 7
    5.29    \item {\tt ISABELLE_LOGIC} setting, 4
    5.30    \item {\tt ISABELLE_OUTPUT} setting, 3, 4
    5.31    \item {\tt ISABELLE_PATH} setting, 3
    5.32    \item {\tt ISABELLE_TMP_PREFIX} setting, 4
    5.33    \item {\tt ISABELLE_TOOLS} setting, 4
    5.34 -  \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 11, 17
    5.35 +  \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 11, 16
    5.36    \item {\tt IsaMakefile}, 10, 11
    5.37    \item {\tt ISATOOL} setting, 3
    5.38    \item {\tt isatool}, 1, 6
    5.39 @@ -50,29 +50,29 @@
    5.40    \indexspace
    5.41  
    5.42    \item {\tt make} tool, 10
    5.43 -  \item {\tt makeall} tool, 10
    5.44 +  \item {\tt makeall} tool, 11
    5.45    \item {\tt ML_HOME} setting, 3
    5.46    \item {\tt ML_OPTIONS} setting, 3
    5.47    \item {\tt ML_SYSTEM} setting, 3
    5.48  
    5.49    \indexspace
    5.50  
    5.51 -  \item {\tt nonascii} tool, 15
    5.52 +  \item {\tt nonascii} tool, 14
    5.53  
    5.54    \indexspace
    5.55  
    5.56    \item settings, \bold{1}
    5.57 -  \item {\tt symbolinput} tool, 16
    5.58 -  \item {\tt symbols}, 14
    5.59 +  \item {\tt symbolinput} tool, 15
    5.60 +  \item {\tt symbols}, 13
    5.61  
    5.62    \indexspace
    5.63  
    5.64 -  \item theory browsing information, \bold{17}
    5.65 -  \item theory graph browser, \bold{18}
    5.66 +  \item theory browsing information, \bold{16}
    5.67 +  \item theory graph browser, \bold{17}
    5.68  
    5.69    \indexspace
    5.70  
    5.71 -  \item {\tt use_dir}, 18
    5.72 +  \item {\tt use_dir}, 17
    5.73    \item {\tt usedir} tool, 11
    5.74  
    5.75  \end{theindex}