Merge PR #12747: Fix coqdoc bad bulleting from incorrect space count

Reviewed-by: Lysxia Reviewed-by: ejgallego Ack-by: ppedrot
author: Emilio Jesus Gallego Arias 2020-07-24 14:44:23 +0200
committer: Emilio Jesus Gallego Arias 2020-07-24 14:44:23 +0200
commit: 55f4095fe3c366a9f310584a55e2dc0605e5409c (patch)
tree: 86bdab378abca78ed7f45fb8cbcf86ba15909b11
parent: 63c216d662647f701daae5e20c5af6ba3e38e3da (diff)
parent: e140848fd50a49aab7810eb369c9e14efe20f2d6 (diff)
5 files changed, 139 insertions, 3 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 0935617fbf..f7447d6cec 100644
--- 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
new file mode 100644
index 0000000000..75dd185ff9
--- /dev/null
+++ 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>
+\ No newline at end of file
diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out
new file mode 100644
index 0000000000..d7eba096fc
--- /dev/null
+++ 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
new file mode 100644
index 0000000000..8ce1faff00
--- /dev/null
+++ 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
index aa3c5b9d3b..b801a3b06e 100644
--- 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
author	Emilio Jesus Gallego Arias	2020-07-24 14:44:23 +0200
committer	Emilio Jesus Gallego Arias	2020-07-24 14:44:23 +0200
commit	55f4095fe3c366a9f310584a55e2dc0605e5409c (patch)
tree	86bdab378abca78ed7f45fb8cbcf86ba15909b11
parent	63c216d662647f701daae5e20c5af6ba3e38e3da (diff)
parent	e140848fd50a49aab7810eb369c9e14efe20f2d6 (diff)