1.1 --- a/doc-src/Ref/syntax.tex	Wed Jul 02 11:59:10 1997 +0200
     1.2 +++ b/doc-src/Ref/syntax.tex	Wed Jul 02 16:46:36 1997 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4  \begin{itemize}
     1.5  \item Name tokens: $\astofpt{t} = \Variable s$, where $t$ is an \ndx{id},
     1.6    \ndx{var}, \ndx{tid}, \ndx{tvar}, \ndx{xnum} or \ndx{xstr} token, and $s$
     1.7 -  its associated string. Note that for {\tt xstr} this does not include the
     1.8 +  its associated string.  Note that for {\tt xstr} this does not include the
     1.9    quotes.
    1.10  
    1.11  \item Copy productions:\index{productions!copy}
    1.12 @@ -606,7 +606,7 @@
    1.13  The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
    1.14  declaration.  Hence {\tt is} is not a logical type and may be used safely as
    1.15  a new nonterminal for custom syntax.  The nonterminal~{\tt is} can later be
    1.16 -re-used for other enumerations of type~{\tt i} like lists or tuples. If we
    1.17 +re-used for other enumerations of type~{\tt i} like lists or tuples.  If we
    1.18  had needed polymorphic enumerations, we could have used the predefined
    1.19  nonterminal symbol \ndx{args} and skipped this part altogether.
    1.20  
    1.21 @@ -850,7 +850,7 @@
    1.22  constraint might appear.
    1.23  
    1.24  Also note that we are responsible to mark free identifiers that
    1.25 -actually represent bound variables. This is achieved by
    1.26 +actually represent bound variables.  This is achieved by
    1.27  \ttindex{Syntax.variant_abs'} and \ttindex{Syntax.mark_boundT} above.
    1.28  Failing to do so may cause these names to be printed in the wrong
    1.29  style.  \index{translations|)} \index{syntax!transformations|)}
    1.30 @@ -861,24 +861,24 @@
    1.31  %
    1.32  Isabelle's meta-logic features quite a lot of different kinds of
    1.33  identifiers, namely {\em class}, {\em tfree}, {\em tvar}, {\em free},
    1.34 -{\em bound}, {\em var}. One might want to have these printed in
    1.35 +{\em bound}, {\em var}.  One might want to have these printed in
    1.36  different styles, e.g.\ in bold or italic, or even transcribed into
    1.37  something more readable like $\alpha, \alpha', \beta$ instead of {\tt
    1.38 -  'a}, {\tt 'aa}, {\tt 'b} for type variables. Token translations
    1.39 +  'a}, {\tt 'aa}, {\tt 'b} for type variables.  Token translations
    1.40  provide a means to such ends, enabling the user to install certain
    1.41  \ML{} functions associated with any logical \rmindex{token class} and
    1.42  depending on some \rmindex{print mode}.
    1.43  
    1.44  The logical class of identifiers can not necessarily be determined by
    1.45 -its syntactic category, though. For example, consider free vs.\ bound
    1.46 -variables. So Isabelle's pretty printing mechanism, starting from
    1.47 +its syntactic category, though.  For example, consider free vs.\ bound
    1.48 +variables.  So Isabelle's pretty printing mechanism, starting from
    1.49  fully typed terms, has to be careful to preserve this additional
    1.50  information\footnote{This is done by marking atoms in abstract syntax
    1.51 -  trees appropriately. The marks are actually visible by print
    1.52 +  trees appropriately.  The marks are actually visible by print
    1.53    translation functions -- they are just special constants applied to
    1.54    atomic asts, for example \texttt{("_bound" x)}.}.  In particular,
    1.55  user-supplied print translation functions operating on terms have to
    1.56 -be well-behaved in this respect. Free identifiers introduced to
    1.57 +be well-behaved in this respect.  Free identifiers introduced to
    1.58  represent bound variables have to be marked appropriately (cf.\ the
    1.59  example at the end of \S\ref{sec:tr_funs}).
    1.60  
    1.61 @@ -890,12 +890,12 @@
    1.62  \end{ttbox}\index{token_translation}
    1.63  The elements of this list are of the form $(m, c, f)$, where $m$ is a
    1.64  print mode identifier, $c$ a token class, and $f\colon string \to
    1.65 -string \times int$ the actual translation function. Assuming that $x$
    1.66 +string \times int$ the actual translation function.  Assuming that $x$
    1.67  is of identifier class $c$, and print mode $m$ is the first one of all
    1.68  currently active modes that provide some translation for $c$, then $x$
    1.69 -is output according to $f(x) = (x', len)$. Thereby $x'$ is the
    1.70 +is output according to $f(x) = (x', len)$.  Thereby $x'$ is the
    1.71  modified identifier name and $len$ its visual length approximated in
    1.72 -terms of whole characters. Thus $x'$ may include non-printing parts
    1.73 +terms of whole characters.  Thus $x'$ may include non-printing parts
    1.74  like control sequences or markup information for typesetting systems.
    1.75  
    1.76  %FIXME example (?)