1.1 --- a/doc-src/Ref/introduction.tex Thu Nov 27 19:37:36 1997 +0100
1.2 +++ b/doc-src/Ref/introduction.tex Thu Nov 27 19:39:02 1997 +0100
1.3 @@ -29,20 +29,19 @@
1.4
1.5 \medskip Let $\langle isabellehome \rangle$ denote the location where
1.6 the distribution has been installed. To run Isabelle from a the shell
1.7 -prompt within an ordinary text terminal session, simply type:
1.8 +prompt within an ordinary text terminal session, simply type
1.9 \begin{ttbox}
1.10 \({\langle}isabellehome{\rangle}\)/bin/isabelle
1.11 \end{ttbox}
1.12 This should start an interactive \ML{} session with the default
1.13 -object-logic already preloaded. All Isabelle commands are bound to
1.14 -\ML{} identifiers.
1.15 +object-logic already preloaded.
1.16
1.17 Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
1.18 has been added to your shell's search path, in order to avoid typing
1.19 full path specifications of the executable files.
1.20
1.21 The object-logic image to load may be also specified explicitly as an
1.22 -argument to the {\tt isabelle} command, e.g.:
1.23 +argument to the {\tt isabelle} command, e.g.
1.24 \begin{ttbox}
1.25 isabelle FOL
1.26 \end{ttbox}
1.27 @@ -50,15 +49,15 @@
1.28 (assuming that {\FOL} has been pre-built).
1.29
1.30 \index{saving your work|bold} Isabelle provides no means of storing
1.31 -theorems or proofs on files. Theorems are simply part of the \ML{}
1.32 -state and are named by \ML{} identifiers. To save your work between
1.33 -sessions, you must dump the \ML{} system state to a file. This is done
1.34 -automatically when ending the session normally (e.g.\ by typing
1.35 -control-D), provided that the image has been opened \emph{writable} in
1.36 -the first place. The standard object-logics are usually read-only, so
1.37 -you probably have to create a private working copy first. For example,
1.38 -the following shell command puts you into a writable Isabelle session
1.39 -of name \texttt{Foo} that initially contains just \FOL:
1.40 +theorems or internal proof objects on files. Theorems are simply part
1.41 +of the \ML{} state. To save your work between sessions, you must dump
1.42 +the \ML{} system state to a file. This is done automatically when
1.43 +ending the session normally (e.g.\ by typing control-D), provided that
1.44 +the image has been opened \emph{writable} in the first place. The
1.45 +standard object-logic images are usually read-only, so you probably
1.46 +have to create a private working copy first. For example, the
1.47 +following shell command puts you into a writable Isabelle session of
1.48 +name \texttt{Foo} that initially contains just \FOL:
1.49 \begin{ttbox}
1.50 isabelle FOL Foo
1.51 \end{ttbox}
1.52 @@ -72,8 +71,8 @@
1.53 isabelle Foo
1.54 \end{ttbox}
1.55
1.56 -More details about \texttt{isabelle} may be found in the \emph{System
1.57 - Manual}.
1.58 +More details about the \texttt{isabelle} command may be found in the
1.59 +\emph{System Manual}.
1.60
1.61 \medskip Saving the state is not enough. Record, on a file, the
1.62 top-level commands that generate your theories and proofs. Such a
1.63 @@ -87,10 +86,8 @@
1.64 \texttt{Isabelle} executable (note the capital I) runs one such
1.65 interface, depending on your local configuration. Furthermore there
1.66 are a number of external utilities available. These are started
1.67 -uniformly via the \texttt{isatool} wrapper.
1.68 -
1.69 -Again, see the \emph{System Manual} for more information user
1.70 -interfaces and utilities.
1.71 +uniformly via the \texttt{isatool} wrapper. See the \emph{System
1.72 + Manual} for more information user interfaces and utilities.
1.73
1.74
1.75 \section{Ending a session}
1.76 @@ -102,9 +99,9 @@
1.77 \begin{ttdescription}
1.78 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
1.79 the state.
1.80 -
1.81 -\item[\ttindexbold{exit}();] same as {\tt quit}, passing a return code
1.82 - to the operating system.
1.83 +
1.84 +\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
1.85 + code \(i\) to the operating system.
1.86
1.87 \item[\ttindexbold{commit}();] saves the current state without ending
1.88 the session, provided that the logic image is opened read-write.
1.89 @@ -123,11 +120,11 @@
1.90 time_use : string -> unit
1.91 \end{ttbox}
1.92 \begin{ttdescription}
1.93 -\item[\ttindexbold{cd} "{\it dir}";]
1.94 - changes the current directory to {\it dir}. This is the default directory
1.95 - for reading files and for writing temporary files.
1.96 -
1.97 -\item[\ttindexbold{pwd}();] returns the path of the current directory.
1.98 +\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
1.99 + {\it dir}. This is the default directory for reading files.
1.100 +
1.101 +\item[\ttindexbold{pwd}();] returns the full path of the current
1.102 + directory.
1.103
1.104 \item[\ttindexbold{use} "$file$";]
1.105 reads the given {\it file} as input to the \ML{} session. Reading a file
1.106 @@ -139,8 +136,8 @@
1.107
1.108 The $dir$ and $file$ specifications of the \texttt{cd} and
1.109 \texttt{use} commands may contain path variables that are expanded
1.110 -accordingly --- e.g.\ \texttt{\$ISABELLE_HOME}, or \texttt{\~\relax}
1.111 -(abbreviating \texttt{\$HOME}). Section~\ref{LoadingTheories}
1.112 +appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
1.113 +(which abbreviates \texttt{\$HOME}). Section~\ref{LoadingTheories}
1.114 describes commands for loading theory files.
1.115
1.116
1.117 @@ -164,8 +161,9 @@
1.118 Pretty.setmargin : int -> unit
1.119 print_depth : int -> unit
1.120 \end{ttbox}
1.121 -These set limits for terminal output. See also {\tt goals_limit}, which
1.122 -limits the number of subgoals printed (page~\pageref{sec:goals-printing}).
1.123 +These set limits for terminal output. See also {\tt goals_limit},
1.124 +which limits the number of subgoals printed
1.125 +(\S\ref{sec:goals-printing}).
1.126
1.127 \begin{ttdescription}
1.128 \item[\ttindexbold{Pretty.setdepth} \(d\);]
1.129 @@ -176,7 +174,7 @@
1.130
1.131 \item[\ttindexbold{Pretty.setmargin} \(m\);]
1.132 tells Isabelle's pretty printer to assume a right margin (page width)
1.133 - of~$m$. The initial margin is~80.
1.134 + of~$m$. The initial margin is~76.
1.135
1.136 \item[\ttindexbold{print_depth} \(n\);]
1.137 limits the printing depth of complex \ML{} values, such as theorems and
1.138 @@ -185,7 +183,7 @@
1.139 \end{ttdescription}
1.140
1.141
1.142 -\subsection{Printing of hypotheses, brackets, types and sorts}
1.143 +\subsection{Printing of hypotheses, brackets, types etc.}
1.144 \index{meta-assumptions!printing of}
1.145 \index{types!printing of}\index{sorts!printing of}
1.146 \begin{ttbox}
1.147 @@ -193,27 +191,38 @@
1.148 show_brackets : bool ref \hfill{\bf initially false}
1.149 show_types : bool ref \hfill{\bf initially false}
1.150 show_sorts : bool ref \hfill{\bf initially false}
1.151 +show_consts : bool ref \hfill{\bf initially false}
1.152 \end{ttbox}
1.153 These flags allow you to control how much information is displayed for
1.154 -terms and theorems. The hypotheses are normally shown; superfluous
1.155 -parentheses are not. Types and sorts are normally hidden. Displaying
1.156 -types and sorts may explain why a polymorphic inference rule fails to
1.157 -resolve with some goal.
1.158 +types, terms and theorems. The hypotheses of theorems \emph{are}
1.159 +normally shown. Superfluous parentheses of types and terms are not.
1.160 +Types and sorts of variables are normally hidden.
1.161 +
1.162 +Note that displaying types and sorts may explain why a polymorphic
1.163 +inference rule fails to resolve with some goal, or why a rewrite rule
1.164 +does not apply as expected.
1.165
1.166 \begin{ttdescription}
1.167 -\item[\ttindexbold{show_hyps} := false;]
1.168 -makes Isabelle show each meta-level hypothesis as a dot.
1.169 +\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
1.170 + meta-level hypothesis as a dot.
1.171 +
1.172 +\item[set \ttindexbold{show_brackets};] makes Isabelle show full
1.173 + bracketing. In particular, this reveals the grouping of infix
1.174 + operators.
1.175 +
1.176 +\item[set \ttindexbold{show_types};] makes Isabelle show types when
1.177 + printing a term or theorem.
1.178 +
1.179 +\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
1.180 + and the sorts of type variables, independently of the value of
1.181 + \texttt{show_types}.
1.182 +
1.183 +\item[set \ttindexbold{show_consts};] makes Isabelle show types of
1.184 + constants, provided that showing of types is enabled at all. This
1.185 + is supported for printing of proof states only. Note that the
1.186 + output can be enormous as polymorphic constants often occur at
1.187 + several different type instances.
1.188
1.189 -\item[\ttindexbold{show_brackets} := true;]
1.190 - makes Isabelle show full bracketing. This reveals the
1.191 - grouping of infix operators.
1.192 -
1.193 -\item[\ttindexbold{show_types} := true;]
1.194 -makes Isabelle show types when printing a term or theorem.
1.195 -
1.196 -\item[\ttindexbold{show_sorts} := true;]
1.197 -makes Isabelle show both types and the sorts of type variables. It does not
1.198 -matter whether {\tt show_types} is also~{\tt true}.
1.199 \end{ttdescription}
1.200
1.201
1.202 @@ -230,7 +239,7 @@
1.203 form.
1.204
1.205 \begin{ttdescription}
1.206 -\item[\ttindexbold{eta_contract} := true;]
1.207 +\item[set \ttindexbold{eta_contract};]
1.208 makes Isabelle perform $\eta$-contractions before printing, so that
1.209 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The
1.210 distinction between a term and its $\eta$-expanded form occasionally
1.211 @@ -238,6 +247,37 @@
1.212 \end{ttdescription}
1.213 \index{printing control|)}
1.214
1.215 +\section{Diagnostic messages}
1.216 +\index{error messages}
1.217 +\index{warnings}
1.218 +
1.219 +Isabelle conceptually provides three output channels for different
1.220 +kinds of messages: ordinary text, warnings, errors. Depending on the
1.221 +user interface involved, these messages may appear in different text
1.222 +styles or colours, even within separate windows.
1.223 +
1.224 +The default setup of an \texttt{isabelle} terminal session is as
1.225 +follows: plain output of ordinary text, warnings prefixed by
1.226 +\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s. For example, a
1.227 +typical warning would look like this:
1.228 +\begin{ttbox}
1.229 +\#\#\# Beware the Jabberwock, my son!
1.230 +\#\#\# The jaws that bite, the claws that catch!
1.231 +\#\#\# Beware the Jubjub Bird, and shun
1.232 +\#\#\# The frumious Bandersnatch!
1.233 +\end{ttbox}
1.234 +
1.235 +\texttt{ML} programs may output diagnostic messages using the
1.236 +following functions:
1.237 +\begin{ttbox}
1.238 +writeln : string -> unit
1.239 +warning : string -> unit
1.240 +error : string -> 'a
1.241 +\end{ttbox}
1.242 +Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
1.243 +after having output the text, while \ttindex{writeln} and
1.244 +\ttindex{warning} resume normal program execution.
1.245 +
1.246
1.247 \section{Displaying exceptions as error messages}
1.248 \index{exceptions!printing of}
1.249 @@ -247,7 +287,7 @@
1.250 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
1.251 and {\tt RSN}, are called both interactively and from programs. They
1.252 indicate errors not by printing messages, but by raising exceptions. For
1.253 -interactive use, \ML's reporting of an uncaught exception is
1.254 +interactive use, \ML's reporting of an uncaught exception may be
1.255 uninformative. The Poly/ML function {\tt exception_trace} can generate a
1.256 backtrace.\index{Poly/{\ML} compiler}
1.257