Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block verbatim from inline verbatim

Reviewed-by: Lysxia

13 files changed, 360 insertions, 102 deletions

diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index 7ab8f9d763..b68b2ed2a7 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -200,6 +200,14 @@ at the beginning of a line.
           if n <= 1 then 1 else n * fact (n-1)
       >>
 
+Verbatim material on a single line is also possible (assuming that
+``>>`` is not part of the text to be presented as verbatim).
+
+.. example::
+
+  ::
+
+      Here is the corresponding caml expression: << fact (n-1) >>
 
 
 Hyperlinks
diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out
index 2b5648aee6..aceccc25fd 100644
--- a/test-suite/coqdoc/binder.tex.out
+++ b/test-suite/coqdoc/binder.tex.out
@@ -20,7 +20,8 @@
 
 \begin{coqdoccode}
 \end{coqdoccode}
-Link binders \begin{coqdoccode}
+Link binders 
+\begin{coqdoccode}
 \coqdocemptyline
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol
diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out
index d7eba096fc..a8f4c254cb 100644
--- a/test-suite/coqdoc/bug12742.tex.out
+++ b/test-suite/coqdoc/bug12742.tex.out
@@ -46,6 +46,7 @@ Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
           xxxxx xxxx xxxxxx.
 
 \end{itemize}
+
 \begin{coqdoccode}
 \end{coqdoccode}
 \end{document}
diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out
index 286e8bba4d..84214a73d3 100644
--- a/test-suite/coqdoc/bug5700.html.out
+++ b/test-suite/coqdoc/bug5700.html.out
@@ -22,8 +22,7 @@
 </div>
 
 <div class="doc">
-<pre>foo (* bar *) </pre>
- 
+<code> foo (* {bar_bar} *) </code> 
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a id="const1" class="idref" href="#const1"><span class="id" title="definition">const1</span></a> := 1.<br/>
@@ -32,8 +31,7 @@
 </div>
 
 <div class="doc">
-<pre>more (* nested (* comments *) within verbatim *) </pre>
- 
+<code> more (* nested (* comments *) within verbatim *) </code> 
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a id="const2" class="idref" href="#const2"><span class="id" title="definition">const2</span></a> := 2.<br/>
diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out
index 1a1af5dfdd..f2b12f0079 100644
--- a/test-suite/coqdoc/bug5700.tex.out
+++ b/test-suite/coqdoc/bug5700.tex.out
@@ -20,14 +20,14 @@
 
 \begin{coqdoccode}
 \end{coqdoccode}
-\begin{verbatim}foo (* bar *) \end{verbatim}
- \begin{coqdoccode}
+\texttt{ foo (* \{bar\_bar\} *) } 
+\begin{coqdoccode}
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol
 \coqdocemptyline
 \end{coqdoccode}
-\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim}
- \begin{coqdoccode}
+\texttt{ more (* nested (* comments *) within verbatim *) } 
+\begin{coqdoccode}
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol
 \end{coqdoccode}
diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v
index 839034a48f..fc985276af 100644
--- a/test-suite/coqdoc/bug5700.v
+++ b/test-suite/coqdoc/bug5700.v
@@ -1,4 +1,4 @@
-(** << foo (* bar *) >> *)
+(** << foo (* {bar_bar} *) >> *)
 Definition const1 := 1.
 
 (** << more (* nested (* comments *) within verbatim *) >> *)
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 2304f5ecc1..412a9ca6ac 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -36,6 +36,7 @@ Various checks for coqdoc
 \item  ``..'' should be rendered correctly
 
 \end{itemize}
+
 \begin{coqdoccode}
 \coqdocemptyline
 \coqdocnoindent
@@ -166,7 +167,8 @@ skip
 
  skip 
 
- skip \begin{coqdoccode}
+ skip 
+\begin{coqdoccode}
 \coqdocemptyline
 \end{coqdoccode}
 \end{document}
diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out
new file mode 100644
index 0000000000..bf9f975ee8
--- /dev/null
+++ b/test-suite/coqdoc/verbatim.html.out
@@ -0,0 +1,114 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>Coqdoc.verbatim</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.verbatim</h1>
+
+<div class="code">
+</div>
+
+<div class="doc">
+
+<div class="paragraph"> </div>
+
+<pre>
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a &gt;&gt; shift;
+}
+</pre>
+
+<div class="paragraph"> </div>
+
+This line and the following shows <code>verbatim </code> text:
+
+<div class="paragraph"> </div>
+
+<code> A stand-alone inline verbatim </code>
+
+<div class="paragraph"> </div>
+
+<code> A non-ended inline verbatim to test line location
+</code>
+
+<div class="paragraph"> </div>
+
+<ul class="doclist">
+<li> item 1
+
+</li>
+<li> item 2 is <code>verbatim</code>
+
+</li>
+<li> item 3 is <code>verbatim</code> too
+<br/>
+<span class="inlinecode"><span class="id" title="var">A</span> <span class="id" title="var">coq</span> <span class="id" title="var">block</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <span class="id" title="var">n</span> = 0
+<div class="paragraph"> </div>
+
+</span>
+</li>
+<li> <code>verbatim</code> again, and a formula <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="var">True</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">False</span></span> <span class="inlinecode"></span>
+
+</li>
+<li>
+<pre>
+multiline
+verbatim
+</pre>
+
+</li>
+<li> last item
+
+</li>
+</ul>
+
+<div class="paragraph"> </div>
+
+<center><table class="infrule">
+<tr class="infruleassumption">
+  <td class="infrule">Γ ⊢ A</td>
+  <td class="infrulenamecol" rowspan="3">
+    &nbsp;
+  </td></tr>
+<tr class="infrulemiddle">
+  <td class="infrule"><hr /></td>
+</tr>
+<tr class="infruleassumption">
+  <td class="infrule">Γ ⊢ A ∨ B</td>
+  <td></td>
+</td>
+</table></center>
+<div class="paragraph"> </div>
+
+<pre>
+A non-ended block verbatim to test line location
+
+*)
+</pre>
+</div>
+<div class="code">
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>
\ No newline at end of file
diff --git a/test-suite/coqdoc/verbatim.tex.out b/test-suite/coqdoc/verbatim.tex.out
new file mode 100644
index 0000000000..b692f6ad6a
--- /dev/null
+++ b/test-suite/coqdoc/verbatim.tex.out
@@ -0,0 +1,84 @@
+\documentclass[12pt]{report}
+\usepackage[utf8x]{inputenc}
+
+%Warning: tipa declares many non-standard macros used by utf8x to
+%interpret utf8 characters but extra packages might have to be added
+%such as "textgreek" for Greek letters not already in tipa
+%or "stmaryrd" for mathematical symbols.
+%Utf8 codes missing a LaTeX interpretation can be defined by using
+%\DeclareUnicodeCharacter{code}{interpretation}.
+%Use coqdoc's option -p to add new packages or declarations.
+\usepackage{tipa}
+
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\begin{document}
+\coqlibrary{Coqdoc.verbatim}{Library }{Coqdoc.verbatim}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+
+
+\begin{verbatim}
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a >> shift;
+}
+\end{verbatim}
+
+
+This line and the following shows \texttt{verbatim } text:
+
+
+\texttt{ A stand-alone inline verbatim }
+
+
+\texttt{ A non-ended inline verbatim to test line location
+}
+
+
+
+\begin{itemize}
+\item  item 1
+
+\item  item 2 is \texttt{verbatim}
+
+\item  item 3 is \texttt{verbatim} too
+\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdocvar{A} \coqdocvar{coq} \coqdocvar{block} : \coqdockw{\ensuremath{\forall}} \coqdocvar{n}, \coqdocvar{n} = 0
+
+\coqdocemptyline
+
+\item  \texttt{verbatim} again, and a formula  \coqdocvar{True} \ensuremath{\rightarrow} \coqdocvar{False} 
+
+\item 
+\begin{verbatim}
+multiline
+verbatim
+\end{verbatim}
+
+\item  last item
+
+\end{itemize}
+
+
+\begin{verbatim}
+Γ ⊢ A
+----
+Γ ⊢ A ∨ B
+\end{verbatim}
+
+
+\begin{verbatim}
+A non-ended block verbatim to test line location
+
+*)
+\end{verbatim}
+\begin{coqdoccode}
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/verbatim.v b/test-suite/coqdoc/verbatim.v
new file mode 100644
index 0000000000..129a5117c9
--- /dev/null
+++ b/test-suite/coqdoc/verbatim.v
@@ -0,0 +1,40 @@
+(**
+
+<<
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a >> shift;
+}
+>>
+
+This line and the following shows << verbatim >> text:
+
+<< A stand-alone inline verbatim >>
+
+<< A non-ended inline verbatim to test line location
+
+
+- item 1
+- item 2 is <<verbatim>>
+- item 3 is <<verbatim>> too
+[[
+A coq block : forall n, n = 0
+]]
+- <<verbatim>> again, and a formula [ True -> False ]
+-
+<<
+multiline
+verbatim
+>>
+- last item
+
+[[[
+Γ ⊢ A
+----
+Γ ⊢ A ∨ B
+]]]
+
+<<
+A non-ended block verbatim to test line location
+
+*)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 5d210b2e60..e5beab5d33 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -278,8 +278,16 @@
           pos_lnum = lcp.pos_lnum + n;
           pos_bol = lcp.pos_cnum }
 
-  let print_position chan p =
-    Printf.fprintf chan "%s:%d:%d" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
+  let print_position_p chan p =
+    Printf.fprintf chan "%s%d, character %d"
+    (if p.pos_fname = "" then "Line " else "File \"" ^ p.pos_fname ^ "\", line ")
+    p.pos_lnum (p.pos_cnum - p.pos_bol)
+
+  let print_position chan {lex_start_p = p} = print_position_p chan p
+
+  let warn msg lexbuf =
+    eprintf "%a, warning: %s\n" print_position lexbuf msg;
+    flush stderr
 
   exception MismatchPreformatted of position
 
@@ -487,29 +495,29 @@ rule coq_bol = parse
         then Output.empty_line_of_code ();
         coq_bol lexbuf }
   | space* "(**" (space_nl as s)
-    { if is_nl s then Lexing.new_line lexbuf;
+    { if is_nl s then new_lines 1 lexbuf;
       Output.end_coq (); Output.start_doc ();
 	let eol = doc_bol lexbuf in
 	  Output.end_doc (); Output.start_coq ();
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | space* "Comments" (space_nl as s)
-      { if is_nl s then Lexing.new_line lexbuf;
+      { if is_nl s then new_lines 1 lexbuf;
         Output.end_coq (); Output.start_doc ();
         comments lexbuf;
         Output.end_doc (); Output.start_coq ();
         coq lexbuf }
   | space* begin_hide nl
-      { Lexing.new_line lexbuf; skip_hide lexbuf; coq_bol lexbuf }
+      { new_lines 1 lexbuf; skip_hide lexbuf; coq_bol lexbuf }
   | space* begin_show nl
-      { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf }
+      { new_lines 1 lexbuf; begin_show (); coq_bol lexbuf }
   | space* end_show nl
-      { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf }
+      { new_lines 1 lexbuf; end_show (); coq_bol lexbuf }
   | space* begin_details (* At this point, the comment remains open,
                             and will be closed by [details_body] *)
       { let s = details_body lexbuf in
         Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf }
   | space* end_details nl
-      { Lexing.new_line lexbuf;
+      { new_lines 1 lexbuf;
         Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf }
   | space* (("Local"|"Global") space+)? gallina_kw_to_hide
       { let s = lexeme lexbuf in
@@ -572,8 +580,7 @@ rule coq_bol = parse
 	  add_printing_token tok s;
 	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
-      { eprintf "warning: bad 'printing' command at character %d\n"
-	  (lexeme_start lexbuf); flush stderr;
+      { warn "bad 'printing' command" lexbuf;
 	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
@@ -582,8 +589,7 @@ rule coq_bol = parse
       { remove_printing_token (lexeme lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+
-      { eprintf "warning: bad 'remove printing' command at character %d\n"
-	  (lexeme_start lexbuf); flush stderr;
+      { warn "bad 'remove printing' command" lexbuf;
 	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
@@ -616,9 +622,9 @@ rule coq_bol = parse
 
 and coq = parse
   | nl
-    { Lexing.new_line lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf }
+    { new_lines 1 lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf }
   | "(**" (space_nl as s)
-    { if is_nl s then Lexing.new_line lexbuf;
+    { if is_nl s then new_lines 1 lexbuf;
       Output.end_coq (); Output.start_doc ();
 	let eol = doc_bol lexbuf in
 	  Output.end_doc (); Output.start_coq ();
@@ -719,7 +725,7 @@ and coq = parse
 
 and doc_bol = parse
   | space* section space+ ([^'\n' '\r' '*'] | '*'+ [^'\n' '\r' ')' '*'])* ('*'+ (nl as s))?
-      { if not (is_none s) then Lexing.new_line lexbuf;
+      { if not (is_none s) then new_lines 1 lexbuf;
         let eol, lex = strip_eol (lexeme lexbuf) in
         let lev, s = sec_title lex in
           if (!Cdglobals.lib_subtitles) &&
@@ -731,7 +737,7 @@ and doc_bol = parse
   | ((space_nl* nl)? as s) (space* '-'+ as line)
       { let nl_count = count_newlines s in
         match check_start_list line with
-          | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf
+          | Neither -> backtrack_past_newline lexbuf; new_lines 1 lexbuf; doc None lexbuf
           | List n ->
               new_lines nl_count lexbuf;
               if nl_count > 0 then Output.paragraph ();
@@ -742,8 +748,10 @@ and doc_bol = parse
       }
   | (space_nl* nl) as s
       { new_lines (count_newlines s) lexbuf; Output.paragraph (); doc_bol lexbuf }
-  | "<<" space*
-      { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf }
+  | "<<" space* nl
+      { new_lines 1 lexbuf; Output.start_verbatim false; verbatim_block lexbuf; doc_bol lexbuf }
+  | "<<"
+      { Output.start_verbatim true; verbatim_inline lexbuf; doc None lexbuf }
   | eof
       { true }
   | '_'
@@ -765,27 +773,33 @@ and doc_list_bol indents = parse
         | InLevel (_,false) ->
             backtrack lexbuf; doc_bol lexbuf
       }
-  | "<<" space*
-      { Output.start_verbatim false;
-        verbatim 0 false lexbuf;
+  | "<<" space* nl
+      { new_lines 1 lexbuf; Output.start_verbatim false;
+        verbatim_block lexbuf;
         doc_list_bol indents lexbuf }
+  | "<<" space*
+      { Output.start_verbatim true;
+        verbatim_inline lexbuf;
+        doc (Some indents) lexbuf }
   | "[[" nl
-      { formatted := Some lexbuf.lex_start_p;
+      { new_lines 1 lexbuf; formatted := Some lexbuf.lex_start_p;
         Output.start_inline_coq_block ();
         ignore(body_bol lexbuf);
         Output.end_inline_coq_block ();
         formatted := None;
         doc_list_bol indents lexbuf }
   | "[[[" nl
-      { inf_rules (Some indents) lexbuf }
+      { new_lines 1 lexbuf; inf_rules (Some indents) lexbuf }
   | space* nl space* '-'
       { (* Like in the doc_bol production, these two productions
            exist only to deal properly with whitespace *)
+        new_lines 1 lexbuf;
         Output.paragraph ();
         backtrack_past_newline lexbuf;
         doc_list_bol indents lexbuf }
   | space* nl space* _
-      { let buf' = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let buf' = lexeme lexbuf in
         let buf =
           let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
             match bufs with
@@ -830,12 +844,14 @@ and doc_list_bol indents = parse
 (*s Scanning documentation elsewhere *)
 and doc indents = parse
   | nl
-      { Output.char '\n';
+      { new_lines 1 lexbuf;
+        Output.char '\n';
         match indents with
         | Some ls -> doc_list_bol ls lexbuf
         | None -> doc_bol lexbuf }
   | "[[" nl
-      { if !Cdglobals.plain_comments
+      { new_lines 1 lexbuf;
+        if !Cdglobals.plain_comments
         then (Output.char '['; Output.char '['; doc indents lexbuf)
         else (formatted := Some lexbuf.lex_start_p;
               Output.start_inline_coq_block ();
@@ -847,7 +863,7 @@ and doc indents = parse
 		  | None -> doc_bol lexbuf
 		else doc indents lexbuf)}
   | "[[[" nl
-      { inf_rules indents lexbuf }
+      { new_lines 1 lexbuf; inf_rules indents lexbuf }
   | "[]"
       { Output.proofbox (); doc indents lexbuf }
   | "{{" { url lexbuf; doc indents lexbuf }
@@ -877,7 +893,7 @@ and doc indents = parse
        doc_bol lexbuf
       }
   | '*'* "*)" space* nl
-      { true }
+      { new_lines 1 lexbuf; Output.char '\n'; true }
   | '*'* "*)"
       { false }
   | "$"
@@ -911,7 +927,7 @@ and doc indents = parse
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
   | "<<" space*
-      { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim true; verbatim_inline lexbuf; doc indents lexbuf }
   | '"'
       { if !Cdglobals.plain_comments 
 	then Output.char '"' 
@@ -951,20 +967,25 @@ and escaped_html = parse
         { backtrack lexbuf }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
-and verbatim depth inline = parse
-  | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
-  | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
-  | ">>" { Output.stop_verbatim inline }
-  | "(*" { Output.verbatim_char inline '(';
-           Output.verbatim_char inline '*';
-           verbatim (depth+1) inline lexbuf }
-  | "*)" { if (depth == 0)
-           then (Output.stop_verbatim inline; backtrack lexbuf)
-           else (Output.verbatim_char inline '*';
-                 Output.verbatim_char inline ')';
-                 verbatim (depth-1) inline lexbuf) }
-  | eof { Output.stop_verbatim inline }
-  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf }
+and verbatim_block = parse
+  | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char false '\n'; Output.stop_verbatim false }
+  | nl ">>"
+        { new_lines 1 lexbuf;
+          warn "missing newline after \">>\" block" lexbuf;
+          Output.verbatim_char false '\n';
+          Output.stop_verbatim false }
+  | eof { warn "unterminated \">>\" block" lexbuf; Output.stop_verbatim false }
+  | nl { new_lines 1 lexbuf; Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf }
+  | _ { Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf }
+
+and verbatim_inline = parse
+  | nl { new_lines 1 lexbuf;
+         warn "unterminated inline \">>\"" lexbuf;
+         Output.char '\n';
+         Output.stop_verbatim true }
+  | ">>" { Output.stop_verbatim true }
+  | eof { warn "unterminated inline \">>\"" lexbuf; Output.stop_verbatim true }
+  | _ { Output.verbatim_char true (lexeme_char lexbuf 0); verbatim_inline lexbuf }
 
 and url = parse
   | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
@@ -993,7 +1014,8 @@ and escaped_coq = parse
                 else skipped_comment lexbuf);
         escaped_coq lexbuf }
   | "*)"
-      { (* likely to be a syntax error: we escape *) backtrack lexbuf }
+      { (* likely to be a syntax error *)
+        warn "unterminated \"]\"" lexbuf; backtrack lexbuf }
   | eof
       { Tokens.flush_sublexer () }
   | identifier
@@ -1036,7 +1058,8 @@ and skipped_comment = parse
       { incr comment_level;
 	skipped_comment lexbuf }
   | "*)" space* nl
-      { decr comment_level;
+      { new_lines 1 lexbuf;
+        decr comment_level;
         if !comment_level > 0 then skipped_comment lexbuf else true }
   | "*)"
       { decr comment_level;
@@ -1050,7 +1073,8 @@ and comment = parse
         Output.start_comment ();
         comment lexbuf }
   | "*)" space* nl
-      { Output.end_comment ();
+      { new_lines 1 lexbuf;
+        Output.end_comment ();
         Output.line_break ();
         decr comment_level;
         if !comment_level > 0 then comment lexbuf else true }
@@ -1064,7 +1088,8 @@ and comment = parse
               escaped_coq lexbuf; Output.end_inline_coq ());
         comment lexbuf }
   | "[[" nl
-      { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
+      { new_lines 1 lexbuf;
+        if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
         else (formatted := Some lexbuf.lex_start_p;
               Output.start_inline_coq_block ();
               let _ = body_bol lexbuf in
@@ -1099,13 +1124,14 @@ and comment = parse
       { Output.indentation (fst (count_spaces (lexeme lexbuf)));
         comment lexbuf }
   | nl
-      { Output.line_break ();
+      { new_lines 1 lexbuf;
+        Output.line_break ();
         comment lexbuf }
   | _ { Output.char (lexeme_char lexbuf 0);
         comment lexbuf }
 
 and skip_to_dot = parse
-  | '.' space* nl { true }
+  | '.' space* nl { new_lines 1 lexbuf; true }
   | eof | '.' space+ { false }
   | "(*"
       { comment_level := 1;
@@ -1114,14 +1140,14 @@ and skip_to_dot = parse
   | _ { skip_to_dot lexbuf }
 
 and skip_to_dot_or_brace = parse
-  | '.' space* nl { true }
+  | '.' space* nl { new_lines 1 lexbuf; true }
   | eof | '.' space+ { false }
   | "(*"
       { comment_level := 1;
         ignore (skipped_comment lexbuf);
         skip_to_dot_or_brace lexbuf }
   | "}" space* nl
-      { true }
+      { new_lines 1 lexbuf; true }
   | "}"
       { false }
   | space*
@@ -1134,7 +1160,7 @@ and body_bol = parse
   | "" { Output.indentation 0; body lexbuf }
 
 and body = parse
-  | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
+  | nl { Tokens.flush_sublexer(); Output.line_break(); new_lines 1 lexbuf; body_bol lexbuf}
   | (nl+ as s) space* "]]" space* nl
       { new_lines (count_newlines s + 1) lexbuf;
         Tokens.flush_sublexer();
@@ -1156,7 +1182,7 @@ and body = parse
           end }
   | "]]" space* nl
       { Tokens.flush_sublexer();
-        Lexing.new_line lexbuf;
+        new_lines 1 lexbuf;
         if is_none !formatted then
           begin
 	    let loc = lexeme_start lexbuf in
@@ -1265,31 +1291,31 @@ and string = parse
   | _      { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf }
 
 and skip_hide = parse
-  | eof | end_hide nl { Lexing.new_line lexbuf; () }
+  | eof | end_hide nl { new_lines 1 lexbuf; () }
   | _ { skip_hide lexbuf }
 
 (*s Reading token pretty-print *)
 
 and printing_token_body = parse
   | "*)" (nl as s)? | eof
-    { if not (is_none s) then Lexing.new_line lexbuf;
+    { if not (is_none s) then new_lines 1 lexbuf;
       let s = Buffer.contents token_buffer in
 	  Buffer.clear token_buffer;
 	  s }
   | (nl | _) as s
-    { if is_nl s then Lexing.new_line lexbuf;
+    { if is_nl s then new_lines 1 lexbuf;
       Buffer.add_string token_buffer (lexeme lexbuf);
 	  printing_token_body lexbuf }
 
 and details_body = parse
   | "*)" space* (nl as s)? | eof
-      { if not (is_none s) then Lexing.new_line lexbuf;
+      { if not (is_none s) then new_lines 1 lexbuf;
         None }
   | ":" space*  { details_body_rec lexbuf }
 
 and details_body_rec = parse
   | "*)" space* (nl as s)? | eof
-        { if not (is_none s) then Lexing.new_line lexbuf;
+        { if not (is_none s) then new_lines 1 lexbuf;
           let s = Buffer.contents token_buffer in
           Buffer.clear token_buffer;
           Some s }
@@ -1300,9 +1326,10 @@ and details_body_rec = parse
     enclosed in [[[  ]]] brackets *)
 and inf_rules indents = parse
   | space* nl     (* blank line, before or between definitions *)
-      { inf_rules indents lexbuf }
+      { new_lines 1 lexbuf; inf_rules indents lexbuf }
   | "]]]" nl      (* end of the inference rules block *)
-      { match indents with
+      { new_lines 1 lexbuf;
+        match indents with
         | Some ls -> doc_list_bol ls lexbuf
         | None -> doc_bol lexbuf }
   | _ 
@@ -1315,7 +1342,8 @@ and inf_rules indents = parse
 *)
 and inf_rules_assumptions indents assumptions = parse
   | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *)
-      { let line = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let line = lexeme lexbuf in
         let (spaces,_) = count_spaces line in
         let dashes_and_name = 
                cut_head_tail_spaces (String.sub line 0 (String.length line - 1))
@@ -1334,7 +1362,8 @@ and inf_rules_assumptions indents assumptions = parse
           inf_rules_conclusion indents (List.rev assumptions) 
                                (spaces, dashes, name) [] lexbuf }
   | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *)
-      { let line = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let line = lexeme lexbuf in
         let (spaces,_) = count_spaces line in
         let assumption = cut_head_tail_spaces 
                             (String.sub line 0 (String.length line - 1))
@@ -1348,11 +1377,12 @@ and inf_rules_assumptions indents assumptions = parse
     blank line or a ']]]'. *)
 and inf_rules_conclusion indents assumptions middle conclusions = parse
   | space* nl | space* "]]]" nl (* end of conclusions. *)
-      { backtrack lexbuf;
+      { new_lines 2 lexbuf; backtrack lexbuf;
         Output.inf_rule assumptions middle (List.rev conclusions);
         inf_rules indents lexbuf }
   | space* [^ '\n']+ nl (* this is a line in the conclusion *)
-      { let line = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let line = lexeme lexbuf in
         let (spaces,_) = count_spaces line in
         let conc = cut_head_tail_spaces (String.sub line 0 
                                                     (String.length line - 1))
@@ -1395,16 +1425,16 @@ and st_subtitle = parse
 {
   (* coq_bol with error handling *)
   let coq_bol' f lb =
-    Lexing.new_line lb; (* Start numbering lines from 1 *)
     try coq_bol lb with
     | MismatchPreformatted p ->
-      Printf.eprintf "%a: mismatched \"[[\"\n" print_position { p with pos_fname = f };
+      Printf.eprintf "%a: mismatched \"[[\"\n" print_position_p p;
       exit 1
 
   let coq_file f m =
     reset ();
     let c = open_in f in
     let lb = from_channel c in
+    let lb = { lb with lex_start_p = { lb.lex_start_p with pos_fname = f } } in
       (Index.current_library := m;
        Output.initialize ();
        Output.start_module ();
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 32cf05e1eb..a87dfb5b2e 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -313,7 +313,7 @@ module Latex = struct
 
   let start_verbatim inline =
     if inline then printf "\\texttt{"
-    else printf "\\begin{verbatim}"
+    else printf "\\begin{verbatim}\n"
 
   let stop_verbatim inline =
     if inline then printf "}"
@@ -479,10 +479,6 @@ module Latex = struct
 
   let end_coq () = printf "\\end{coqdoccode}\n"
 
-  let start_code () = end_doc (); start_coq ()
-
-  let end_code () = end_coq (); start_doc ()
-
   let section_kind = function
     | 1 -> "\\section{"
     | 2 -> "\\subsection{"
@@ -632,11 +628,11 @@ module Html = struct
   let stop_quote () = start_quote ()
 
   let start_verbatim inline =
-    if inline then printf "<tt>"
-    else printf "<pre>"
+    if inline then printf "<code>"
+    else printf "<pre>\n"
 
   let stop_verbatim inline =
-    if inline then printf "</tt>"
+    if inline then printf "</code>"
     else printf "</pre>\n"
 
   let url addr name =
@@ -738,7 +734,7 @@ module Html = struct
 
   let end_doc () = in_doc := false;
     stop_item ();
-    if not !raw_comments then printf "\n</div>\n"
+    if not !raw_comments then printf "</div>\n"
 
   let start_emph () = printf "<i>"
 
@@ -754,10 +750,6 @@ module Html = struct
 
   let end_comment () = printf "*)</span>"
 
-  let start_code () = end_doc (); start_coq ()
-
-  let end_code () = end_coq (); start_doc ()
-
   let start_inline_coq () =
     if !inline_notmono then printf "<span class=\"inlinecodenm\">"
                        else printf "<span class=\"inlinecode\">"
@@ -1069,9 +1061,6 @@ module TeXmacs = struct
   let start_comment () = ()
   let end_comment () = ()
 
-  let start_code () = in_doc := true; printf "<\\code>\n"
-  let end_code () = in_doc := false; printf "\n</code>"
-
   let section_kind = function
     | 1 -> "section"
     | 2 -> "subsection"
@@ -1181,9 +1170,6 @@ module Raw = struct
   let start_coq () = ()
   let end_coq () = ()
 
-  let start_code () = end_doc (); start_coq ()
-  let end_code () = end_coq (); start_doc ()
-
   let section_kind =
     function
       | 1 -> "* "
@@ -1240,9 +1226,6 @@ let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment
 let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
 let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
 
-let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code
-let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code
-
 let start_inline_coq =
   select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq
 let end_inline_coq =
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index b7a8d4d858..4088fdabf7 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -41,9 +41,6 @@ val end_comment : unit -> unit
 val start_coq : unit -> unit
 val end_coq : unit -> unit
 
-val start_code : unit -> unit
-val end_code : unit -> unit
-
 val start_inline_coq : unit -> unit
 val end_inline_coq : unit -> unit