Fix coqdoc bad bulleting from incorrect space count

Fix #12742 (cherry picked from commit e140848)
coq · Jul 24, 2020 · 302705c · 302705c
1 parent 5486c72
commit 302705c
Show file tree

Hide file tree

Showing 5 changed files with 139 additions and 3 deletions.
diff --git a/test-suite/Makefile b/test-suite/Makefile
@@ -771,8 +771,6 @@ coq-makefile/%.log : coq-makefile/%/run.sh
 
 # coqdoc
 
-coqdoc: $(patsubst %.sh,%.log,$(wildcard coqdoc/*.sh))
-
 $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \

diff --git a/test-suite/coqdoc/bug12742.html.out b/test-suite/coqdoc/bug12742.html.out
@@ -0,0 +1,67 @@
+<!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.bug12742</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.bug12742</h1>
+
+<div class="code">
+</div>
+
+<div class="doc">
+Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
+     xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx.
+     Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx
+     xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx.  Xxxxx xxxxx
+     xxxx xxxx xxx xxxxx xxxxxxxxxx:
+
+<div class="paragraph"> </div>
+
+<ul class="doclist">
+<li> <i>Xxxxxxxxx xxxxxxx xxxxxxx</i> xxxxxxx "xxxx-xxxxxx" xxxxxxxxx:
+          xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx <i>xxxx</i> xx
+          <i>xxxxx</i> (xx, xxxxxxxxx, <i>xxx'x xxxx: xxx xxx xx xxxx</i>).
+          Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx
+          xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx
+          xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx.  Xxxxxxxx xx xxxx
+          xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx.
+
+<div class="paragraph"> </div>
+
+
+</li>
+<li> <i>Xxxxx xxxxxxxxxx</i> xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx
+          xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx
+          xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx.  Xxxxxx xxxx xxxxx
+          xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx,
+          xxxxx xxxx xxxxxx.
+
+</li>
+</ul>
+
+</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>
diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out
@@ -0,0 +1,51 @@
+\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.bug12742}{Library }{Coqdoc.bug12742}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
+     xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx.
+     Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx
+     xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx.  Xxxxx xxxxx
+     xxxx xxxx xxx xxxxx xxxxxxxxxx:
+
+
+
+\begin{itemize}
+\item  \textit{Xxxxxxxxx xxxxxxx xxxxxxx} xxxxxxx ``xxxx-xxxxxx'' xxxxxxxxx:
+          xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx \textit{xxxx} xx
+          \textit{xxxxx} (xx, xxxxxxxxx, \textit{xxx'x xxxx: xxx xxx xx xxxx}).
+          Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx
+          xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx
+          xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx.  Xxxxxxxx xx xxxx
+          xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx.
+
+
+
+\item  \textit{Xxxxx xxxxxxxxxx} xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx
+          xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx
+          xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx.  Xxxxxx xxxx xxxxx
+          xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx,
+          xxxxx xxxx xxxxxx.
+
+\end{itemize}
+\begin{coqdoccode}
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/bug12742.v b/test-suite/coqdoc/bug12742.v
@@ -0,0 +1,20 @@
+ (** Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
+     xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx.
+     Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx
+     xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx.  Xxxxx xxxxx
+     xxxx xxxx xxx xxxxx xxxxxxxxxx:
+
+        - _Xxxxxxxxx xxxxxxx xxxxxxx_ xxxxxxx "xxxx-xxxxxx" xxxxxxxxx:
+          xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx _xxxx_ xx
+          _xxxxx_ (xx, xxxxxxxxx, _xxx'x xxxx: xxx xxx xx xxxx_).
+          Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx
+          xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx
+          xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx.  Xxxxxxxx xx xxxx
+          xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx.
+
+        - _Xxxxx xxxxxxxxxx_ xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx
+          xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx
+          xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx.  Xxxxxx xxxx xxxxx
+          xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx,
+          xxxxx xxxx xxxxxx.
+*)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
@@ -728,7 +728,7 @@ and doc_bol = parse
           else
             Output.section lev (fun () -> ignore (doc None (from_string s)));
 	    if eol then doc_bol lexbuf else doc None lexbuf }
-  | (space_nl* as s) ('-'+ as line)
+  | ((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