grammars with links (html only)

git-svn-id: http://caml.inria.fr/svn/ocamldoc/trunk@10114 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

23 files changed, 236 insertions, 167 deletions

diff --git a/manual/manual/Makefile b/manual/manual/Makefile
index dacf99bdcb..45e79b6f3b 100644
--- a/manual/manual/Makefile
+++ b/manual/manual/Makefile
@@ -6,11 +6,11 @@ TEXFONTS=../../styles:
 RELEASE=$$HOME/release/$${RELEASENAME}
 CSLDIR=../../cslrel
 OCAMLDOC=$(CSLDIR)/ocamldoc/ocamldoc.opt -hide Pervasives 
-HEVEA=hevea -v -fix -exec xxdate.exe
+HEVEA=hevea
 HACHA=hacha
-INFO=-info -w 79
-HTML=-O
-TEXT=-text -w 79
+INFO=-fix -exec xxdate.exe -info -w 79
+HTML=-fix -exec xxdate.exe -O
+TEXT=-fix -exec xxdate.exe -text -w 79
 
 CSLDIR2=../$(CSLDIR)
 MLIS=$(CSLDIR2)/stdlib/*.mli \
diff --git a/manual/manual/cmds/debugger.etex b/manual/manual/cmds/debugger.etex
index a2c58a849c..868f52d927 100644
--- a/manual/manual/cmds/debugger.etex
+++ b/manual/manual/cmds/debugger.etex
@@ -359,16 +359,16 @@ are in scope at the selected program point can be accessed.
 Expressions that can be printed are a subset of Objective Caml
 expressions, as described by the following grammar:
 \begin{syntax}
-expr:
+simple-expr:
     lowercase-ident
   | { capitalized-ident '.' } lowercase-ident
   | '*'
   | '$' integer
-  | expr '.' lowercase-ident
-  | expr '.(' integer ')'
-  | expr '.[' integer ']'
-  | '!' expr
-  | '(' expr ')'
+  | simple-expr '.' lowercase-ident
+  | simple-expr '.(' integer ')'
+  | simple-expr '.[' integer ']'
+  | '!' simple-expr
+  | '(' simple-expr ')'
 \end{syntax}
 The first two cases refer to a value identifier, either unqualified or
 qualified by the path to the structure that define it.
diff --git a/manual/manual/cmds/intf-c.etex b/manual/manual/cmds/intf-c.etex
index bdc647f121..1c6aa51de3 100644
--- a/manual/manual/cmds/intf-c.etex
+++ b/manual/manual/cmds/intf-c.etex
@@ -1,4 +1,4 @@
-\chapter{Interfacing C with Objective Caml} \label{c:intf-c}
+\chapter{Interfacing\label{c:intf-c} C with Objective Caml}
 \pdfchapterfold{-9}{Interfacing C with Objective Caml}
 
 This chapter describes how user-defined primitives, written in C, can
@@ -8,7 +8,6 @@ be linked with Caml code and called from Caml functions.
 \pdfsection{Overview and compilation information}
 
 \subsection{Declaring primitives}
-
 User primitives are declared in an implementation file or
 "struct"\ldots"end" module expression using the "external" keyword:
 \begin{alltt}
diff --git a/manual/manual/cmds/lexyacc.etex b/manual/manual/cmds/lexyacc.etex
index f1933126fc..d70856c787 100644
--- a/manual/manual/cmds/lexyacc.etex
+++ b/manual/manual/cmds/lexyacc.etex
@@ -139,32 +139,35 @@ may facilitate the use of "ocamllex" as a simple text processing tool.
 
 The regular expressions are in the style of "lex", with a more
 Caml-like syntax.
-
+\begin{syntax}
+regexp:
+  \ldots
+\end{syntax}
 \begin{options}
 
-\item[@"'" char "'"@]
+\item[@"'" regular-char || escape-sequence "'"@]
 A character constant, with the same syntax as Objective Caml character
 constants. Match the denoted character.
 
 \item["_"]
 (Underscore.) Match any character.
 
-\item["eof"]
+\item[@"eof"@]
 Match the end of the lexer input.\\
 {\bf Note:} On some systems, with interactive input, an end-of-file
 may be followed by more characters.  However, "ocamllex" will not
 correctly handle regular expressions that contain "eof" followed by
 something else.
 
-\item[@'"' string '"'@]
+\item[@'"' { string-character } '"'@]
 A string constant, with the same syntax as Objective Caml string
 constants. Match the corresponding sequence of characters.
 
 \item[@'[' character-set ']'@]
 Match any single character belonging to the given
 character set. Valid character sets are: single
-character constants @"'" c "'"@; ranges of characters
-@"'" c_1 "'" "-" "'" c_2 "'"@ (all characters between $c_1$ and $c_2$,
+character constants @"'" @c@ "'"@; ranges of characters
+@"'" @c@_1 "'" "-" "'" @c@_2 "'"@ (all characters between $c_1$ and $c_2$,
 inclusive); and the union of two or more character sets, denoted by
 concatenation.
 
@@ -266,7 +269,7 @@ alternation of those. Then, the type of @ident@ is "char" (or "char
 option").
 Option types are introduced when overall rule matching does not
 imply matching of the bound sub-pattern. This is in particular the
-case of @'(' regexp 'as' indent')' '?'@ and of
+case of @'(' regexp 'as' ident ')' '?'@ and of
 @regexp_1 '|' '(' regexp_2 'as' ident ')'@.
 
 There is no linearity restriction over "as" bound variables.
@@ -357,20 +360,22 @@ Declarations are given one per line. They all start with a \verb"%" sign.
 
 \begin{options}
 
-\item[@"%token" symbol \ldots symbol@]
-Declare the given symbols as tokens (terminal symbols).  These symbols
+\item[@"%token" constr \ldots constr@]
+Declare the given symbols @constr \ldots constr@
+as tokens (terminal symbols).  These symbols
 are added as constant constructors for the "token" concrete type.
 
-\item[@"%token" "<" type ">" symbol \ldots symbol@]
-Declare the given symbols as tokens with an attached attribute of the
+\item[@"%token" "<" typexpr ">" constr \ldots constr@]
+Declare the given symbols @constr \ldots constr@ as tokens with an
+attached attribute of the
 given type. These symbols are added as constructors with arguments of
-the given type for the "token" concrete type. The @type@ part is
+the given type for the "token" concrete type. The @typexpr@ part is
 an arbitrary Caml type expression, except that all type
 constructor names must be fully qualified (e.g. "Modname.typename")
 for all types except standard built-in types, even if the proper
 \verb|open| directives (e.g. \verb|open Modname|) were given in the
 header section. That's because the header is copied only to the ".ml"
-output file, but not to the ".mli" output file, while the @type@ part
+output file, but not to the ".mli" output file, while the @typexpr@ part
 of a \verb"%token" declaration is copied to both.
 
 \item[@"%start" symbol \ldots symbol@]
@@ -380,12 +385,12 @@ output module. Non-terminals that are not declared as entry points
 have no such parsing function. Start symbols must be given a type with
 the \verb|%type| directive below.
 
-\item[@"%type" "<" type ">" symbol \ldots symbol@]
+\item[@"%type" "<" typexpr ">" symbol \ldots symbol@]
 Specify the type of the semantic attributes for the given symbols.
 This is mandatory for start symbols only. Other nonterminal symbols
 need not be given types by hand: these types will be inferred when
 running the output files through the Objective Caml compiler (unless the
-\verb"-s" option is in effect). The @type@ part is an arbitrary Caml
+\verb"-s" option is in effect). The @typexpr@ part is an arbitrary Caml
 type expression, except that all type constructor names must be
 fully qualified, as explained above for "%token".
 
diff --git a/manual/manual/cmds/top.etex b/manual/manual/cmds/top.etex
index 1ac795b44b..0ab949846a 100644
--- a/manual/manual/cmds/top.etex
+++ b/manual/manual/cmds/top.etex
@@ -21,20 +21,12 @@ toplevel-phrase:
         | expr
         | '#' ident directive-argument
 ;
-definition:
-          'let' ['rec'] let-binding  { 'and' let-binding }
-        | 'external' value-name ':' typexpr '=' external-declaration
-        | type-definition
-        | exception-definition
-        | 'module' module-name [ ':' module-type ] '=' module-expr
-        | 'module' 'type' modtype-name '=' module-type
-        | 'open' module-path
-;
 directive-argument:
-          nothing
+          epsilon
         | string-literal
         | integer-literal
         | value-path
+;
 \end{syntax}
 
 A phrase can consist of a definition, similar to those found in
@@ -90,7 +82,7 @@ easily be used in conjunction with an external line editor such as
 \end{latexonly}
 \begin{htmlonly}
 (see the
-\ahref{http://caml.inria.fr/humps/index_framed_caml.html}{Caml Hump}).
+\ahref{http://caml.inria.fr/humps/index\_framed\_caml.html}{Caml Hump}).
 \end{htmlonly}
 Another option is to use "ocaml" under Gnu Emacs, which gives the
 full editing power of Emacs (command "run-caml" from library "inf-caml").
@@ -249,12 +241,12 @@ type of the function. That is, the toplevel loop will call
 \var{printer-name} when it has such a value to print.
 
 The printing function \var{printer-name} should have type
-@"Format.formatter" "->" t "->" "unit"@, where \var{t} is the
+@"Format.formatter" "->" @t@ "->" "unit"@, where @@t@@ is the
 type for the values to be printed, and should output its textual
-representation for the value of type \var{t} on the given formatter,
+representation for the value of type @@t@@ on the given formatter,
 using the functions provided by the "Format" library.  For backward
 compatibility, \var{printer-name} can also have type
-@t "->" "unit"@ and should then output on the standard
+@@t@ "->" "unit"@ and should then output on the standard
 formatter, but this usage is deprecated.
 
 \item["#remove_printer "\var{printer-name}";;"]
diff --git a/manual/manual/library/tk.mli b/manual/manual/library/tk.mli
index f83c169558..d3c8d199fa 100644
--- a/manual/manual/library/tk.mli
+++ b/manual/manual/library/tk.mli
@@ -2,7 +2,6 @@
 
 (** Basic functions and types for LablTk *)
 
-open Tk
 open Widget
 
 (** {6 Initialization and termination} *)
diff --git a/manual/manual/macros.hva b/manual/manual/macros.hva
index d95e349e9d..682741ddfb 100644
--- a/manual/manual/macros.hva
+++ b/manual/manual/macros.hva
@@ -8,27 +8,6 @@
 \newcommand{\endcaml}{\activebracetrue\end{alltt}}
 \renewcommand{\:}{\renewcommand{\?}{\@zyva}\maroon}
 \newcommand{\var}[1]{\textit{#1}}
-\newif\ifspace
-\def\addspace{\ifspace\;\spacefalse\fi}
-\newcommand{\token}[1]{\texttt{\blue#1}}
-\def\nonterm#1{\addspace\texttt{\sl#1}\spacetrue}
-\def\brepet{\addspace\{}
-\def\erepet{\}}
-\def\boption{\addspace[}
-\def\eoption{]}
-\def\brepets{\addspace\{}
-\def\erepets{\}^+}
-\def\bparen{\addspace(}
-\def\eparen{)}
-\def\orelse{\mid \spacefalse}
-\def\is{ & ::= & \spacefalse }
-\def\alt{ \\ & \mid & \spacefalse }
-\def\sep{ \\[2mm] \spacefalse }
-\def\cutline{}
-\def\emptystring{\epsilon}
-\def\syntax{$$\begin{array}{rrl}\spacefalse}
-\def\endsyntax{\end{array}$$}
-\def\synt#1{$\spacefalse#1$}
 
 \newenvironment{library}{}{}
 \newcounter{page}
@@ -107,7 +86,7 @@
 
 \newcommand{\vfill}{}
 \def\number{}
-\def\year{2004}
+\def\year{2005}
 
 % Pour alltt
 
@@ -117,5 +96,4 @@
 
 \def\@savedlistI{}
 
-%pour ocamldocdescription
-\newcommand{\moduleref}[1]{\ifouthtml\ahref{libref/#1.html}{\texttt{#1}}}
+
diff --git a/manual/manual/manual.hva b/manual/manual/manual.hva
index 9a18bb5296..4c8d59d93e 100644
--- a/manual/manual/manual.hva
+++ b/manual/manual/manual.hva
@@ -1,5 +1,4 @@
 \input{book.hva}
 \input{fancysection.hva}
-\newcounter{tocdepth}
 \input{macros.hva}
 \newif\ifouthtml\outhtmltrue
\ No newline at end of file
diff --git a/manual/manual/manual.inf b/manual/manual/manual.inf
index 3aac5c5c41..784249097e 100644
--- a/manual/manual/manual.inf
+++ b/manual/manual/manual.inf
@@ -1,7 +1,6 @@
 \input{book.hva}
 \renewcommand{\@indexsection}[1]{\chapter{#1}}
 \newcommand{\black}{\htmlcolor{#000000}}
-\newcounter{tocdepth}
 \newcommand{\machine}{\tt}
 \newenvironment{camlunder}{\@style{U}}{}
 \newcommand{\caml}{\begin{alltt}\renewcommand{\\}{\char92}\def\<{\begin{camlunder}}\renewcommand{\>}{\end{camlunder}}\activebracefalse}
@@ -9,26 +8,6 @@
 \newcommand{\?}{\black\#\blue }
 \renewcommand{\:}{\maroon}
 \newcommand{\var}[1]{\textit{#1}}
-\newif\ifspace
-\def\addspace{\ifspace\spacefalse\fi}
-\newcommand{\token}[1]{\texttt{\blue#1}}
-\def\nonterm#1{\addspace\texttt{\sl#1}\spacetrue}
-\def\brepet{\addspace\{}
-\def\erepet{\}}
-\def\boption{\addspace[}
-\def\eoption{]}
-\def\brepets{\addspace\{}
-\def\erepets{\}^+}
-\def\bparen{\addspace(}
-\def\eparen{)}
-\def\orelse{\mid\spacefalse}
-\def\is{ & ::= & \spacefalse }
-\def\alt{ \\ & \mid & \spacefalse }
-\def\sep{ \\[2mm] \spacefalse }
-\def\emptystring{\epsilon}
-\def\syntax{$$\begin{array}{rrl}\spacefalse}
-\def\endsyntax{\end{array}$$}
-\def\synt#1{$\spacefalse#1$}
 
 \newenvironment{library}{}{}
 \newcounter{page}
@@ -120,11 +99,9 @@
 \def\event{§§}
 \def\fromoneto#1#2{$#1 = 1,\ldots{} , #2$}
 
-\newcommand{\jobname}{manual}
 \newcommand{\vfill}{}
-
-%\def\number{}
-%\def\year{2003}
+\def\number{}
+\def\year{2005}
 
 % Pour alltt
 
diff --git a/manual/manual/refman/classes.etex b/manual/manual/refman/classes.etex
index 12e12e7831..a6eda25e8f 100644
--- a/manual/manual/refman/classes.etex
+++ b/manual/manual/refman/classes.etex
@@ -171,7 +171,9 @@ class-expr:
    |  'let' ['rec'] let-binding {'and' let-binding} 'in' class-expr
    |  'object' ['(' pattern [':' typexpr] ')'] { class-field } 'end'
 ;
+%BEGIN LATEX
 \end{syntax} \begin{syntax}
+%END LATEX
 class-field:
       'inherit' class-expr ['as' value-name]
    |  'val' ['mutable'] inst-var-name [':' typexpr] '=' expr
@@ -233,11 +235,12 @@ is a short form for
 The {\tt let} and {\tt let rec} constructs bind value names locally,
 as for the core language expressions.
 
-\subsubsection*{Class body}
-\label{ss:class-body}
-
+\subsubsection*{Class\label{ss:class-body} body}
+\begin{syntax}
+class-body:  ['(' pattern [':' typexpr] ')'] { class-field }
+\end{syntax}
 The expression
-@'object' '(' pattern [':' typexpr] ')' { class-field } 'end'@ denotes
+@'object' class-body 'end'@ denotes
 a class body. This is the prototype for an object : it lists the
 instance variables and methods of an objet of this class.
 
@@ -462,7 +465,7 @@ defines an abbreviation @class-name@ for the class body type
 @class-body-type@.  As for class definitions, two type abbreviations
 @class-name@ and @'#' class-name@ are also defined. The definition can
 be parameterized by some type parameters. If any method in the class
-type body is virtual, the definition must be flagged @virtual@.
+type body is virtual, the definition must be flagged "virtual".
 
 Two class type definitions match if they have the same type parameters
 and the types they expand to match.
diff --git a/manual/manual/refman/compunit.etex b/manual/manual/refman/compunit.etex
index a35960d197..3ec3790d20 100644
--- a/manual/manual/refman/compunit.etex
+++ b/manual/manual/refman/compunit.etex
@@ -31,10 +31,10 @@ interface or unit implementation must not have any other free variables.
 In other terms, the type-checking and compilation of an interface or
 implementation proceeds in the initial environment
 \begin{center}
-@name_1 ':' 'sig' interface_1 'end' \ldots
- name_n ':' 'sig' interface_n 'end'@
+@name_1 ':' 'sig' specification_1 'end' \ldots
+ name_n ':' 'sig' specification_n 'end'@
 \end{center}
 where @name_1 \ldots name_n@ are the names of the other
 compilation units available in the search path (see
-chapter~\ref{c:camlc} for more details) and @interface_1 \ldots
-interface_n@ are their respective interfaces.
+chapter~\ref{c:camlc} for more details) and @specification_1 \ldots
+specification_n@ are their respective interfaces.
diff --git a/manual/manual/refman/expr.etex b/manual/manual/refman/expr.etex
index 7ba5e6920f..51def7ee82 100644
--- a/manual/manual/refman/expr.etex
+++ b/manual/manual/refman/expr.etex
@@ -1,4 +1,4 @@
-\section{Expressions} \label{s:value-expr}
+\section{Expressions\label{s:value-expr}}
 \pdfsection{Expressions}
 \ikwd{in\@\texttt{in}|see{\texttt{let}}}
 \ikwd{and\@\texttt{and}|see{\texttt{let}, \texttt{type}, \texttt{class}}}
@@ -59,7 +59,7 @@ expr:
   | 'try' expr 'with' pattern-matching
   | 'let' ['rec'] let-binding  { 'and' let-binding } 'in' expr
   | 'new' class-path
-  | 'object' ['(' pattern [':' typexpr] ')'] { class-field } 'end'
+  | 'object' class-body 'end'
   | expr '#' method-name
   | inst-var-name
   | inst-var-name '<-' expr
@@ -69,7 +69,9 @@ expr:
   | 'assert' expr
   | 'lazy' expr
 ;
+%BEGIN LATEX
 \end{syntax} \begin{syntax}
+%END LATEX
 argument:
     expr
   | '~' label-name
@@ -157,10 +159,12 @@ is good style to use @'begin' \ldots 'end'@ inside control structures:
 and @'(' \ldots ')'@ for the other grouping situations.
 
 Parenthesized expressions can contain a type constraint, as in @'('
-expr ':' type ')'@. This constraint forces the type of @expr@ to be
-compatible with @type@.
+expr ':' typexpr ')'@. This constraint forces the type of @expr@ to be
+compatible with @typexpr@.
 
-Parenthesized expressions can also contain coercions @'(' expr [':' type] ':>' type')'@ (see subsection~\ref{s:objects} below).
+Parenthesized expressions can also contain coercions
+@'(' expr [':' typexpr] ':>' typexpr')'@ (see
+subsection~\ref{s:objects} below).
 
 
 \subsubsection*{Function application}
@@ -169,7 +173,7 @@ Function application is denoted by juxtaposition of (possibly labeled)
 expressions. The expression @expr argument_1 \ldots argument_n@
 evaluates the expression @expr@ and those appearing in @argument_1@
 to @argument_n@. The expression @expr@ must evaluate to a
-functional value @f@, which is then applied to the values of 
+functional value $f$, which is then applied to the values of 
 @argument_1, \ldots, argument_n@.
 
 The order in which the expressions @expr, argument_1, \ldots,
@@ -192,7 +196,7 @@ passed for them.
 All other missing parameters (without corresponding argument), both
 optional and non-optional, will be kept, and the result of the
 function will still be a function of these missing parameters to the
-body of @f@.
+body of $f$.
 
 As a special case, if the function has a known arity, all the
 arguments are unlabeled, and their number matches the number of
@@ -245,13 +249,14 @@ This expression is equivalent to:
 \end{center}
 Functions of the form @"fun" optlabel '(' pattern '=' expr_0 ')' '->'
 expr@ are equivalent to
-\begin{syntax}
-"fun" optlabel x '->'
+\begin{center}
+@"fun" optlabel ident '->'
   "let" pattern '='
-    "match" x "with" "Some" x "->" x '|' "None" '->' expr_0
-  "in" expr
-\end{syntax}
-where @x@ is a fresh variable. When @expr_0@ will be evaluated is left
+    "match" ident "with" "Some" ident "->" ident '|' "None" '->' expr_0
+  "in" expr@
+\end{center}
+where @ident@
+is a fresh variable. When @expr_0@ will be evaluated is left
 unspecified.
 
 After these two transformations, expressions are of the form
@@ -503,8 +508,8 @@ tag is @tag-name@, and whose argument is the value of @expr@.
 
 The expression @'{' field_1 '=' expr_1 ';' \ldots ';' field_n '='
 expr_n '}'@ evaluates to the record value
-@'{' field_1 '=' v_1 ';' \ldots ';' field_n '=' v_n '}'@,
-where @v_i@ is the value of @expr_i@ for \fromoneto{i}{n}.
+$\{ field_1 = v_1; \ldots; field_n = v_n \}$
+where $v_i$ is the value of @expr_i@ for \fromoneto{i}{n}.
 The fields @field_1@ to @field_n@ must all belong to the same record
 types; all fields belonging to this record type must appear exactly
 once in the record expression, though they can appear in any
@@ -644,9 +649,9 @@ returning a new object of this class.
 
 Creating directly an object through the @'object' class-body 'end'@
 construct is operationally equivalent to defining locally a @'class'
-myclass '=' 'object' class-body 'end'@ ---see sections
+class-name '=' 'object' class-body 'end'@ ---see sections
 \ref{ss:class-body} and following for the syntax of @class-body@---
-and immediately creating a single object from it by @'new' myclass@.
+and immediately creating a single object from it by @'new' class-name@.
 
 The typing of immediate objects is slightly different from explicitely
 defining a class in two respects. First, the inferred object type may
@@ -679,15 +684,15 @@ variable @inst-var-name@, which must be mutable.  The whole expression
 
 The type of an object can be coerced (weakened) to a supertype.
 %
-The expression @'(' expr ':>' typexpr ')'@ coerces the expression @expr@
+The expression @'('expr ':>' typexpr')'@ coerces the expression @expr@
 to type @typexpr@.
 %
-The expression @'(' expr ':' typexpr_1 ':>' typexpr_2 ')'@ coerces the
+The expression @'('expr ':' typexpr_1 ':>' typexpr_2')'@ coerces the
 expression @expr@ from type @typexpr_1@ to type @typexpr_2@.
 %
 The former operator will sometimes fail to coerce an expression @expr@
-from a type @t_1@ to a type @t_2@ even if type @t_1@ is a subtype of type
-@t_2@: in the current implementation it only expands two levels of
+from a type $t_1$ to a type $t_2$ even if type $t_1$ is a subtype of type
+$t_2$: in the current implementation it only expands two levels of
 type abbreviations containing objects and/or variants, keeping only
 recursion when it is explicit in the class type. In case of failure,
 the latter operator should be used.
diff --git a/manual/manual/refman/exten.etex b/manual/manual/refman/exten.etex
index 8c9bd5e623..bfbab9fbd9 100644
--- a/manual/manual/refman/exten.etex
+++ b/manual/manual/refman/exten.etex
@@ -62,16 +62,16 @@ It will be accepted if each one of @expr_1 \ldots expr_n@ is
 statically constructive with respect to @name_1 \ldots name_n@ and
 not immediately linked to any of @name_1 \ldots name_n@
 
-An expression @e@ is said to be {\em statically constructive
+An expression @@e@@ is said to be {\em statically constructive
 with respect to} the variables @name_1 \ldots name_n@ if at least
 one of the following conditions is true:
 \begin{itemize}
-\item @e@ has no free occurrence of any of @name_1 \ldots name_n@
-\item @e@ is a variable
-\item @e@ has the form @"fun" \ldots "->" \ldots@
-\item @e@ has the form @"function" \ldots "->" \ldots@
-\item @e@ has the form @"lazy" "(" \ldots ")"@
-\item @e@ has one of the following forms, where each one of
+\item @@e@@ has no free occurrence of any of @name_1 \ldots name_n@
+\item @@e@@ is a variable
+\item @@e@@ has the form @"fun" \ldots "->" \ldots@
+\item @@e@@ has the form @"function" \ldots "->" \ldots@
+\item @@e@@ has the form @"lazy" "(" \ldots ")"@
+\item @@e@@ has one of the following forms, where each one of
   @expr_1 \ldots expr_m@ is statically constructive with respect to
   @name_1 \ldots name_n@, and @expr_0@ is statically constructive with
   respect to @name_1 \ldots name_n, xname_1 \ldots xname_m@:
@@ -91,13 +91,13 @@ one of the following conditions is true:
   \end{itemize}
 \end{itemize}
 
-An expression @e@ is said to be {\em immediately linked to} the variable
+An expression @@e@@ is said to be {\em immediately linked to} the variable
 @name@ in the following cases:
 \begin{itemize}
-\item @e@ is @name@
-\item @e@ has the form @expr_1";" \ldots ";" expr_m@ where @expr_m@
+\item @@e@@ is @name@
+\item @@e@@ has the form @expr_1";" \ldots ";" expr_m@ where @expr_m@
    is immediately linked to @name@
-\item @e@ has the form @"let" ["rec"] xname_1 "=" expr_1 "and" \ldots
+\item @@e@@ has the form @"let" ["rec"] xname_1 "=" expr_1 "and" \ldots
    "and" xname_m "=" expr_m "in" expr_0@ where @expr_0@ is immediately
    linked to @name@ or to one of the @xname_i@ such that @expr_i@
    is immediately linked to @name@.
@@ -106,11 +106,11 @@ An expression @e@ is said to be {\em immediately linked to} the variable
 \section{Range patterns}
 
 In patterns, Objective Caml recognizes the form
-@"'" c "'" ".." "'" d "'"@
+@"'" @c@ "'" ".." "'" @d@ "'"@
 (two character literals separated by~"..") as shorthand for the pattern
 \begin{center}
-@"'" c "'" "|" "'" c_1 "'" "|" "'" c_2 "'" "|" \ldots
-        "|" "'" c_n "'" "|" "'" d "'"@
+@"'" @c@ "'" "|" "'" @c@_1 "'" "|" "'" @c@_2 "'" "|" \ldots
+        "|" "'" @c@_n "'" "|" "'" @d@ "'"@
 \end{center}
 where \nth{c}{1}, \nth{c}{2}, \ldots, \nth{c}{n} are the characters
 that occur between \var{c} and \var{d} in the ASCII character set. For
@@ -264,10 +264,10 @@ not final and subject to change in future releases.
 Currently, the compiler requires that all dependency cycles between
 the recursively-defined module identifiers go through at least one
 ``safe'' module.  A module is ``safe'' if all value definitions that
-it contains have function types @ty_1 '->' ty_2@.  Evaluation of a
+it contains have function types @typexpr_1 '->' typexpr_2@.  Evaluation of a
 recursive module definition proceeds by building initial values for
 the safe modules involved, binding all (functional) values to
-@'fun' x '->' 'raise' 'Undefined_recursive_module'@.  The defining
+@'fun' '_' '->' 'raise' 'Undefined_recursive_module'@.  The defining
 module expressions are then evaluated, and the initial values
 for the safe modules are replaced by the values thus computed.  If a
 function component of a safe module is applied during this computation
diff --git a/manual/manual/refman/modtypes.etex b/manual/manual/refman/modtypes.etex
index 1c5ccdc927..9a963537cf 100644
--- a/manual/manual/refman/modtypes.etex
+++ b/manual/manual/refman/modtypes.etex
@@ -29,8 +29,10 @@ mod-constraint:
           'type' [type-parameters] typeconstr '=' typexpr
         | 'module' module-path '=' extended-module-path
 ;
+%BEGIN LATEX
 \end{syntax}
 \begin{syntax}
+%END LATEX
 specification:
           'val' value-name ':' typexpr
         | 'external' value-name ':' typexpr '=' external-declaration
@@ -95,8 +97,8 @@ written @'type' typedef { 'and' typedef }@ and consists of a sequence
 of mutually recursive definitions of type names.
 
 Each type definition in the signature specifies an optional type
-equation @'=' typexp@ and an optional type representation 
-@'=' constr-decl \ldots@ or @'=' '{' label-decl \ldots '}'@.
+equation @'=' typexpr@ and an optional type representation 
+@'=' constr-decl \ldots@ or @'=' '{' field-decl \ldots '}'@.
 The implementation of the type name in a matching structure must
 be compatible with the type expression specified in the equation (if
 given), and have the specified representation (if given). Conversely,
@@ -118,10 +120,10 @@ right-hand side of the abbreviation will be hidden from the users of the
 structure. Users of the structure consider that type as incompatible
 with any other type: a fresh type has been generated.
 
-\item[Type abbreviation: an equation @'=' typexp@, no representation.] ~ \\
-The type name must be implemented by a type compatible with @typexp@.
+\item[Type abbreviation: an equation @'=' typexpr@, no representation.] ~ \\
+The type name must be implemented by a type compatible with @typexpr@.
 All users of the structure know that the type name is
-compatible with @typexp@.
+compatible with @typexpr@.
 
 \item[New variant type or record type: no equation, a representation.] ~ \\
 The type name must be implemented by a variant type or record type
@@ -255,7 +257,7 @@ Assuming @module-type@ denotes a signature, the expression
 the same signature where type equations have been added to some of the
 type specifications, as described by the constraints following the
 "with" keyword. The constraint @'type' [type-parameters] typeconstr
-'=' typexp@  adds the type equation @'=' typexp@ to the specification
+'=' typexpr@  adds the type equation @'=' typexpr@ to the specification
 of the type component named @typeconstr@ of the constrained signature.
 The constraint @'module' module-path '=' extended-module-path@ adds
 type equations to all type components of the sub-structure denoted by
diff --git a/manual/manual/refman/modules.etex b/manual/manual/refman/modules.etex
index 43ca357982..7a6fdc01f0 100644
--- a/manual/manual/refman/modules.etex
+++ b/manual/manual/refman/modules.etex
@@ -1,4 +1,4 @@
-\section{Module expressions (module implementations)} \label{s:module-expr}
+\section{Module\label{s:module-expr} expressions (module implementations)}
 \pdfsection{Module expressions (module implementations)}
 
 Module expressions are the module-level equivalent of value
diff --git a/manual/manual/refman/patterns.etex b/manual/manual/refman/patterns.etex
index 7340452517..6f54e9a655 100644
--- a/manual/manual/refman/patterns.etex
+++ b/manual/manual/refman/patterns.etex
@@ -70,7 +70,7 @@ The pattern @"(" pattern_1 ")"@ matches the same values as
 @pattern_1@. A type constraint can appear in a
 parenthesized pattern, as in @"(" pattern_1 ":" typexpr ")"@. This
 constraint forces the type of @pattern_1@ to be compatible with
-@type@.
+@typexpr@.
 
 \subsubsection*{``Or'' patterns}
 
@@ -81,9 +81,9 @@ matches @pattern_2@. The two sub-patterns @pattern_1@ and @pattern_2@
 must bind exactly the same identifiers to values having the same types.
 Matching is performed from left to right.
 More precisely,
-in case some value~@v@ matches @pattern_1 "|" pattern_2@, the bindings 
-performed are those of @pattern_1@ when @v@ matches @pattern_1@.
-Otherwise, value~@v@ matches  @pattern_2@ whose bindings are performed.
+in case some value~$v$ matches @pattern_1 "|" pattern_2@, the bindings 
+performed are those of @pattern_1@ when $v$ matches @pattern_1@.
+Otherwise, value~$v$ matches  @pattern_2@ whose bindings are performed.
 
 
 \subsubsection*{Variant patterns}
@@ -108,18 +108,18 @@ whose tag is equal to @tag-name@, and whose argument matches
 
 \subsubsection*{Variant abbreviation patterns}
 
-If the type @["('a,'b,...)"] typeconstr = "[`tag"_1 t_1 "|"
-\ldots "|" "`tag"_n t_n"]"@ is defined, then the pattern @\#typeconstr@
-is a shorthand for the or-pattern @"(`tag"_1"(_" ":" t_1")" "|"
-\ldots "|" "`tag"_n"(_" ":" t_n"))"@. It matches all values of type
+If the type @["('a,'b,...)"] typeconstr = "[`tag"_1 typexpr_1 "|"
+\ldots "|" "`tag"_n typexpr_n"]"@ is defined, then the pattern @\#typeconstr@
+is a shorthand for the or-pattern @"(`tag"_1"(_" ":" typexpr_1")" "|"
+\ldots "|" "`tag"_n"(_" ":" typexpr_n"))"@. It matches all values of type
 @\#typeconstr@.
 
 \subsubsection*{Tuple patterns}
 
 The pattern @pattern_1 "," \ldots "," pattern_n@ matches $n$-tuples
 whose components match the patterns @pattern_1@ through @pattern_n@. That
-is, the pattern matches the tuple values @(v_1, \ldots, v_n)@ such that
-@pattern_i@ matches @v_i@ for \fromoneto{i}{n}.
+is, the pattern matches the tuple values $(v_1, \ldots, v_n)$ such that
+@pattern_i@ matches $v_i$ for \fromoneto{i}{n}.
 
 \subsubsection*{Record patterns}
 
@@ -134,6 +134,6 @@ into account for matching.
 \subsubsection*{Array patterns}
 
 The pattern @"[|" pattern_1 ";" \ldots ";" pattern_n "|]"@
-matches arrays of length @n@ such that the @i@-th array element
+matches arrays of length $n$ such that the $i$-th array element
 matches the pattern @pattern_i@, for \fromoneto{i}{n}.
 
diff --git a/manual/manual/refman/refman.etex b/manual/manual/refman/refman.etex
index cf1447f6f2..ee22b5fcbe 100644
--- a/manual/manual/refman/refman.etex
+++ b/manual/manual/refman/refman.etex
@@ -20,7 +20,7 @@ definitely part of a full formal definition of the language.
 
 The syntax of the language is given in BNF-like notation. Terminal
 symbols are set in typewriter font (@'like' 'this'@).
-Non-terminal symbols are set in italic font (@like that@). 
+Non-terminal symbols are set in italic font (@@like@ @that@@). 
 Square brackets @[\ldots]@ denote optional components. Curly brackets
 @{\ldots}@ denotes zero, one or several repetitions of the enclosed
 components. Curly bracket with a trailing plus sign @{{\ldots}}@
diff --git a/manual/manual/refman/types.etex b/manual/manual/refman/types.etex
index 81f6411936..d9b54ff915 100644
--- a/manual/manual/refman/types.etex
+++ b/manual/manual/refman/types.etex
@@ -133,7 +133,9 @@ tag-spec:
         '`'tag-name [ "of" typexpr ]
       | typexpr
 ;
+%BEGIN LATEX
 \end{syntax} \begin{syntax}
+%END LATEX
 tag-spec-full:
         '`'tag-name [ "of" typexpr ] { '&' typexpr }
       | typexpr
diff --git a/manual/manual/refman/values.etex b/manual/manual/refman/values.etex
index a3407d81f8..1562cd95ef 100644
--- a/manual/manual/refman/values.etex
+++ b/manual/manual/refman/values.etex
@@ -80,7 +80,7 @@ The current implementation limits each variant type to have at most
 Polymorphic variants are an alternate form of variant values, not
 belonging explicitly to a predefined variant type, and following
 specific typing rules. They can be either constant, written
-@"`"tag-name@, or non-constant, written @"`"tag-name(v)@.
+@"`"tag-name@, or non-constant, written @"`"tag-name@$(v)$.
 
 \subsection{Functions}
 
diff --git a/manual/styles/ocamldoc.hva b/manual/styles/ocamldoc.hva
index 902834265d..58b7bb1219 100644
--- a/manual/styles/ocamldoc.hva
+++ b/manual/styles/ocamldoc.hva
@@ -2,18 +2,19 @@
 \newenvironment{ocamldoccode}{\begin{alltt}}{\end{alltt}}
 \newenvironment{ocamldocdescription}{\begin{quote}}{\end{quote}}
 \newenvironment{ocamldoccomment}{\begin{quote}}{\end{quote}}
-\newcommand\textbar{|}
-\newcommand\textbackslash{\begin{rawhtml}\\end{rawhtml}}
-\newcommand\textasciicircum{\^{}}
-\newcommand\sharp{#}
 
 
 \newenvironment{ocamldocindent}{\list{}{}\item\relax}{\endlist}
 \newenvironment{ocamldocsigend}
      {\noindent\quad\texttt{sig}\ocamldocindent}
-     {\endocamldocindent\vskip -\lastskip
+     {\endocamldocindent
       \noindent\quad\texttt{end}\medskip}
 \newenvironment{ocamldocobjectend}
      {\noindent\quad\texttt{object}\ocamldocindent}
-     {\endocamldocindent\vskip -\lastskip
+     {\endocamldocindent
       \noindent\quad\texttt{end}\medskip}
+
+\newcommand{\moduleref}[1]{\ifhtml\ahref{libref/#1.html}{\texttt{#1}}\fi}
+
+# For processing .tex generated by ocamldoc (for text manual)
+\newcommand{\ocamldocvspace}[1]{\vspace{#1}}
\ No newline at end of file
diff --git a/manual/styles/syntaxdef.hva b/manual/styles/syntaxdef.hva
new file mode 100644
index 0000000000..828dda7e15
--- /dev/null
+++ b/manual/styles/syntaxdef.hva
@@ -0,0 +1,100 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Hevea code for syntax definitions of the ocaml manual %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Important commands
+% \token, for typesetting grammar terminals
+% \nonterm, for typesetting grammar non-terminals
+%
+% Beware: \nonterm introduces either a local anchor or a local reference
+%   -Anchors are introduced when \nonterm occurs in the first column of
+%    syntax definitions (environment 'syntax')
+%   - References are introduced everywhere else
+%
+% For pure typesetting effect without links (eg. to typeset 'e' as 'expr') 
+% use the \nt command (eg. \nt{e}).
+% In syntax definitions, the tool 'transf' translates @word@ into \nt{word}.
+%
+% Warnings are produced
+%  - For references to non-defined non terminals
+%  - For multiple definitions of the same non-terminal
+% Warnings can be avoided for a given non-terminal 'expr' by issuing
+% the command \stx@silent{'expr'}
+\newif\ifspace
+\def\addspace{\ifspace\;\spacefalse\fi}
+\ifhtml
+\newcommand{\token}[1]{\texttt{\blue#1}}
+\else
+\newcommand{\token}[1]{\texttt{#1}}
+\fi
+%%% warnings
+\def\stx@warning#1#2{\@ifundefined{stx@#1@silent}{\warning{#2}}{}}
+\def\stx@silent#1{\def\csname stx@#1@silent\endcsname{}}
+%%% Do not warn about those
+%Not defined
+\stx@silent{regular-char}%
+\stx@silent{regular-char-str}%
+\stx@silent{lowercase-ident}%
+\stx@silent{capitalized-ident}%
+%utilities used in many places
+\stx@silent{prefix}%
+\stx@silent{name}%
+\stx@silent{xname}%
+\stx@silent{cond}%
+%Not defined
+\stx@silent{external-declaration}%
+\stx@silent{unit-name}%
+%%Redefined in exten.etex
+\stx@silent{expr}%
+\stx@silent{type-representation}%
+\stx@silent{definition}%
+\stx@silent{specification}%
+\stx@silent{type-equation}%
+%%Not really defined in lexyacc.etex
+\stx@silent{character-set}%
+\stx@silent{symbol}%
+%%Not defined in debugger.etex
+\stx@silent{integer}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%Refer to anchor
+\def\ref@anchor#1{%
+\@ifundefined{stx@#1@exists}
+{\stx@warning{#1}{Undefined non-terminal: '#1'}#1}
+{\ahrefloc{#1}{#1}}}
+\def\stx@exists#1{\def\csname stx@#1@exists\endcsname{}}
+%%Define anachor
+\def\def@anchor#1{%
+\@ifundefined{stx@#1}
+{{\@nostyle\@auxdowrite{\string\stx@exists\{#1\}}}%
+\gdef\csname stx@#1\endcsname{}\aname{#1}{#1}}
+{\@ifundefined{stx@#1@silent}
+{\warning{Redefinition of non-terminal '#1'}#1}
+{\ref@anchor{#1}}}}
+%%%Change \@anchor and initial definition, for html only, of course!
+\ifhtml
+\def\set@name{\let\@anchor\def@anchor}
+\let\@anchor\ref@anchor
+\else
+\def\set@name{}
+\def\@anchor{}
+\fi
+%%%Format non-terminal
+\def\nt#1{\textit{\maroon#1}}
+%%%Link for non-terminal and format
+\def\nonterm#1{\addspace\nt{\@anchor{#1}}\spacetrue}
+\def\brepet{\addspace\{}
+\def\erepet{\}}
+\def\boption{\addspace[}
+\def\eoption{]}
+\def\brepets{\addspace\{}
+\def\erepets{\}^+}
+\def\bparen{\addspace(}
+\def\eparen{)}
+\def\orelse{\mid \spacefalse}
+\def\is{ & ::= & \spacefalse }
+\def\alt{ \\ & \mid & \spacefalse }
+\def\sep{ \\ \\ \spacefalse }
+\def\cutline{}
+\def\emptystring{\epsilon}
+\def\syntax{$$\begin{array}{>{\set@name}rcl}\spacefalse}
+\def\endsyntax{\end{array}$$}
+\def\synt#1{$\spacefalse#1$}
diff --git a/manual/styles/syntaxdef.sty b/manual/styles/syntaxdef.sty
index bb17b94a7d..216c5ed2a4 100644
--- a/manual/styles/syntaxdef.sty
+++ b/manual/styles/syntaxdef.sty
@@ -1,7 +1,8 @@
 \newif\ifspace
 \def\addspace{\ifspace \; \spacefalse \fi}
 \def\token#1{\addspace\hbox{\tt #1} \spacetrue}
-\def\nonterm#1{\addspace\hbox{\sl #1\/} \spacetrue}
+\def\nonterm#1{\addspace\nt{#1} \spacetrue}
+\def\nt#1{\hbox{\sl #1\/}}
 \def\brepet{\addspace\{}
 \def\erepet{\}}
 \def\boption{\addspace[}
diff --git a/manual/tools/transf.mll b/manual/tools/transf.mll
index 0bd11ad049..201d1dbd54 100644
--- a/manual/tools/transf.mll
+++ b/manual/tools/transf.mll
@@ -29,11 +29,17 @@ and syntax = parse
       print_string "\\token{";
       indoublequote lexbuf }
   | "epsilon" { print_string "\\emptystring"; syntax lexbuf }
-  | ['a'-'z'] ['a'-'z' '0'-'9' '-'] * {
+  | ['a'-'z'] ['a'-'z' '0'-'9' '-'] * as lxm {
       print_string "\\nonterm{";
-      print_string (lexeme lexbuf);
+      print_string lxm ;
+      print_string"}";
+      syntax lexbuf }
+  | '@' (['a'-'z'] ['a'-'z' '0'-'9' '-'] * as lxm) '@' {
+      print_string "\\nt{";
+      print_string lxm ;
       print_string"}";
       syntax lexbuf }
+
   | '\\' ['a'-'z''A'-'Z'] + {
       print_string (lexeme lexbuf);
       syntax lexbuf }