
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/introduction.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -29,20 +29,19 @@
 
 \medskip Let $\langle isabellehome \rangle$ denote the location where
 the distribution has been installed.  To run Isabelle from a the shell
-prompt within an ordinary text terminal session, simply type:
+prompt within an ordinary text terminal session, simply type
 \begin{ttbox}
 \({\langle}isabellehome{\rangle}\)/bin/isabelle
 \end{ttbox}
 This should start an interactive \ML{} session with the default
-object-logic already preloaded.  All Isabelle commands are bound to
-\ML{} identifiers.
+object-logic already preloaded.
 
 Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
 has been added to your shell's search path, in order to avoid typing
 full path specifications of the executable files.
 
 The object-logic image to load may be also specified explicitly as an
-argument to the {\tt isabelle} command, e.g.:
+argument to the {\tt isabelle} command, e.g.
 \begin{ttbox}
 isabelle FOL
 \end{ttbox}
@@ -50,15 +49,15 @@
 (assuming that {\FOL} has been pre-built).
 
 \index{saving your work|bold} Isabelle provides no means of storing
-theorems or proofs on files.  Theorems are simply part of the \ML{}
-state and are named by \ML{} identifiers.  To save your work between
-sessions, you must dump the \ML{} system state to a file.  This is done
-automatically when ending the session normally (e.g.\ by typing
-control-D), provided that the image has been opened \emph{writable} in
-the first place.  The standard object-logics are usually read-only, so
-you probably have to create a private working copy first.  For example,
-the following shell command puts you into a writable Isabelle session
-of name \texttt{Foo} that initially contains just \FOL:
+theorems or internal proof objects on files.  Theorems are simply part
+of the \ML{} state.  To save your work between sessions, you must dump
+the \ML{} system state to a file.  This is done automatically when
+ending the session normally (e.g.\ by typing control-D), provided that
+the image has been opened \emph{writable} in the first place.  The
+standard object-logic images are usually read-only, so you probably
+have to create a private working copy first.  For example, the
+following shell command puts you into a writable Isabelle session of
+name \texttt{Foo} that initially contains just \FOL:
 \begin{ttbox}
 isabelle FOL Foo
 \end{ttbox}
@@ -72,8 +71,8 @@
 isabelle Foo  
 \end{ttbox}
 
-More details about \texttt{isabelle} may be found in the \emph{System
-  Manual}.
+More details about the \texttt{isabelle} command may be found in the
+\emph{System Manual}.
 
 \medskip Saving the state is not enough.  Record, on a file, the
 top-level commands that generate your theories and proofs.  Such a
@@ -87,10 +86,8 @@
 \texttt{Isabelle} executable (note the capital I) runs one such
 interface, depending on your local configuration.  Furthermore there
 are a number of external utilities available.  These are started
-uniformly via the \texttt{isatool} wrapper.
-
-Again, see the \emph{System Manual} for more information user
-interfaces and utilities.
+uniformly via the \texttt{isatool} wrapper.  See the \emph{System
+  Manual} for more information user interfaces and utilities.
 
 
 \section{Ending a session}
@@ -102,9 +99,9 @@
 \begin{ttdescription}
 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
   the state.
-
-\item[\ttindexbold{exit}();] same as {\tt quit}, passing a return code
-  to the operating system.
+  
+\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
+  code \(i\) to the operating system.
 
 \item[\ttindexbold{commit}();] saves the current state without ending
   the session, provided that the logic image is opened read-write.
@@ -123,11 +120,11 @@
 time_use        : string -> unit
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{cd} "{\it dir}";]
-  changes the current directory to {\it dir}.  This is the default directory
-  for reading files and for writing temporary files.
-
-\item[\ttindexbold{pwd}();] returns the path of the current directory.
+\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
+  {\it dir}.  This is the default directory for reading files.
+  
+\item[\ttindexbold{pwd}();] returns the full path of the current
+  directory.
 
 \item[\ttindexbold{use} "$file$";]  
 reads the given {\it file} as input to the \ML{} session.  Reading a file
@@ -139,8 +136,8 @@
 
 The $dir$ and $file$ specifications of the \texttt{cd} and
 \texttt{use} commands may contain path variables that are expanded
-accordingly --- e.g.\ \texttt{\$ISABELLE_HOME}, or \texttt{\~\relax}
-(abbreviating \texttt{\$HOME}).  Section~\ref{LoadingTheories}
+appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
+(which abbreviates \texttt{\$HOME}).  Section~\ref{LoadingTheories}
 describes commands for loading theory files.
 
 
@@ -164,8 +161,9 @@
 Pretty.setmargin : int -> unit
 print_depth      : int -> unit
 \end{ttbox}
-These set limits for terminal output.  See also {\tt goals_limit}, which
-limits the number of subgoals printed (page~\pageref{sec:goals-printing}).
+These set limits for terminal output.  See also {\tt goals_limit},
+which limits the number of subgoals printed
+(\S\ref{sec:goals-printing}).
 
 \begin{ttdescription}
 \item[\ttindexbold{Pretty.setdepth} \(d\);]  
@@ -176,7 +174,7 @@
 
 \item[\ttindexbold{Pretty.setmargin} \(m\);]  
   tells Isabelle's pretty printer to assume a right margin (page width)
-  of~$m$.  The initial margin is~80.
+  of~$m$.  The initial margin is~76.
 
 \item[\ttindexbold{print_depth} \(n\);]  
   limits the printing depth of complex \ML{} values, such as theorems and
@@ -185,7 +183,7 @@
 \end{ttdescription}
 
 
-\subsection{Printing of hypotheses, brackets, types and sorts}
+\subsection{Printing of hypotheses, brackets, types etc.}
 \index{meta-assumptions!printing of}
 \index{types!printing of}\index{sorts!printing of}
 \begin{ttbox} 
@@ -193,27 +191,38 @@
 show_brackets : bool ref \hfill{\bf initially false}
 show_types    : bool ref \hfill{\bf initially false}
 show_sorts    : bool ref \hfill{\bf initially false}
+show_consts   : bool ref \hfill{\bf initially false}
 \end{ttbox}
 These flags allow you to control how much information is displayed for
-terms and theorems.  The hypotheses are normally shown; superfluous
-parentheses are not.  Types and sorts are normally hidden.  Displaying
-types and sorts may explain why a polymorphic inference rule fails to
-resolve with some goal.
+types, terms and theorems.  The hypotheses of theorems \emph{are}
+normally shown.  Superfluous parentheses of types and terms are not.
+Types and sorts of variables are normally hidden.
+
+Note that displaying types and sorts may explain why a polymorphic
+inference rule fails to resolve with some goal, or why a rewrite rule
+does not apply as expected.
 
 \begin{ttdescription}
-\item[\ttindexbold{show_hyps} := false;]   
-makes Isabelle show each meta-level hypothesis as a dot.
+\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
+  meta-level hypothesis as a dot.
+  
+\item[set \ttindexbold{show_brackets};] makes Isabelle show full
+  bracketing.  In particular, this reveals the grouping of infix
+  operators.
+  
+\item[set \ttindexbold{show_types};] makes Isabelle show types when
+  printing a term or theorem.
+  
+\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
+  and the sorts of type variables, independently of the value of
+  \texttt{show_types}.
+  
+\item[set \ttindexbold{show_consts};] makes Isabelle show types of
+  constants, provided that showing of types is enabled at all.  This
+  is supported for printing of proof states only.  Note that the
+  output can be enormous as polymorphic constants often occur at
+  several different type instances.
 
-\item[\ttindexbold{show_brackets} := true;] 
-  makes Isabelle show full bracketing.  This reveals the
-  grouping of infix operators.
-
-\item[\ttindexbold{show_types} := true;]
-makes Isabelle show types when printing a term or theorem.
-
-\item[\ttindexbold{show_sorts} := true;]
-makes Isabelle show both types and the sorts of type variables.  It does not
-matter whether {\tt show_types} is also~{\tt true}. 
 \end{ttdescription}
 
 
@@ -230,7 +239,7 @@
 form.
 
 \begin{ttdescription}
-\item[\ttindexbold{eta_contract} := true;]
+\item[set \ttindexbold{eta_contract};]
 makes Isabelle perform $\eta$-contractions before printing, so that
 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
 distinction between a term and its $\eta$-expanded form occasionally
@@ -238,6 +247,37 @@
 \end{ttdescription}
 \index{printing control|)}
 
+\section{Diagnostic messages}
+\index{error messages}
+\index{warnings}
+
+Isabelle conceptually provides three output channels for different
+kinds of messages: ordinary text, warnings, errors.  Depending on the
+user interface involved, these messages may appear in different text
+styles or colours, even within separate windows.
+
+The default setup of an \texttt{isabelle} terminal session is as
+follows: plain output of ordinary text, warnings prefixed by
+\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
+typical warning would look like this:
+\begin{ttbox}
+\#\#\# Beware the Jabberwock, my son!
+\#\#\# The jaws that bite, the claws that catch!
+\#\#\# Beware the Jubjub Bird, and shun
+\#\#\# The frumious Bandersnatch!
+\end{ttbox}
+
+\texttt{ML} programs may output diagnostic messages using the
+following functions:
+\begin{ttbox}
+writeln : string -> unit
+warning : string -> unit
+error   : string -> 'a
+\end{ttbox}
+Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
+after having output the text, while \ttindex{writeln} and
+\ttindex{warning} resume normal program execution.
+
 
 \section{Displaying exceptions as error messages}
 \index{exceptions!printing of}
@@ -247,7 +287,7 @@
 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
 and {\tt RSN}, are called both interactively and from programs.  They
 indicate errors not by printing messages, but by raising exceptions.  For
-interactive use, \ML's reporting of an uncaught exception is 
+interactive use, \ML's reporting of an uncaught exception may be
 uninformative.  The Poly/ML function {\tt exception_trace} can generate a
 backtrace.\index{Poly/{\ML} compiler}
 




