aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--test-suite/coqdoc/bug5700.html.out50
-rw-r--r--test-suite/coqdoc/bug5700.tex.out24
-rw-r--r--test-suite/coqdoc/bug5700.v5
-rw-r--r--tools/coqdoc/cpretty.mll19
4 files changed, 92 insertions, 6 deletions
diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out
new file mode 100644
index 000000000..0e05660d6
--- /dev/null
+++ b/test-suite/coqdoc/bug5700.html.out
@@ -0,0 +1,50 @@
+<!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=iso-8859-1" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>Coqdoc.bug5700</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.bug5700</h1>
+
+<div class="code">
+</div>
+
+<div class="doc">
+<pre>foo (* bar *) </pre>
+
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="const1"><span class="id" title="definition">const1</span></a> := 1.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+<pre>more (* nested (* comments *) within verbatim *) </pre>
+
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="const2"><span class="id" title="definition">const2</span></a> := 2.<br/>
+</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/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out
new file mode 100644
index 000000000..33990cb89
--- /dev/null
+++ b/test-suite/coqdoc/bug5700.tex.out
@@ -0,0 +1,24 @@
+\documentclass[12pt]{report}
+\usepackage[]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\begin{document}
+\coqlibrary{Coqdoc.bug5700}{Library }{Coqdoc.bug5700}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+\begin{verbatim}foo (* bar *) \end{verbatim}
+ \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}
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v
new file mode 100644
index 000000000..839034a48
--- /dev/null
+++ b/test-suite/coqdoc/bug5700.v
@@ -0,0 +1,5 @@
+(** << foo (* bar *) >> *)
+Definition const1 := 1.
+
+(** << more (* nested (* comments *) within verbatim *) >> *)
+Definition const2 := 2.
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 60a245dc4..186f6cf6c 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -682,7 +682,7 @@ and doc_bol = parse
| space* nl+
{ Output.paragraph (); doc_bol lexbuf }
| "<<" space*
- { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
+ { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf }
| eof
{ true }
| '_'
@@ -707,7 +707,7 @@ and doc_list_bol indents = parse
}
| "<<" space*
{ Output.start_verbatim false;
- verbatim false lexbuf;
+ verbatim 0 false lexbuf;
doc_list_bol indents lexbuf }
| "[[" nl
{ formatted := true;
@@ -852,7 +852,7 @@ and doc indents = parse
Output.char (lexeme_char lexbuf 1);
doc indents lexbuf }
| "<<" space*
- { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+ { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf }
| '"'
{ if !Cdglobals.plain_comments
then Output.char '"'
@@ -892,13 +892,20 @@ and escaped_html = parse
{ backtrack lexbuf }
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
-and verbatim inline = parse
+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.stop_verbatim inline; backtrack lexbuf }
+ | "(*" { 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 inline lexbuf }
+ | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf }
and url = parse
| "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }