From e140848fd50a49aab7810eb369c9e14efe20f2d6 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Jul 2020 11:29:36 +0200 Subject: Fix coqdoc bad bulleting from incorrect space count Fix #12742 --- test-suite/Makefile | 2 -- test-suite/coqdoc/bug12742.html.out | 67 +++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/bug12742.tex.out | 51 ++++++++++++++++++++++++++++ test-suite/coqdoc/bug12742.v | 20 +++++++++++ 4 files changed, 138 insertions(+), 2 deletions(-) create mode 100644 test-suite/coqdoc/bug12742.html.out create mode 100644 test-suite/coqdoc/bug12742.tex.out create mode 100644 test-suite/coqdoc/bug12742.v (limited to 'test-suite') 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 @@ + + + + + +Coqdoc.bug12742 + + + + +
+ + + +
+ +

Library Coqdoc.bug12742

+ +
+
+ +
+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. + +
    • +
+ +
+
+
+
+ + + +
+ + + \ 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. +*) -- cgit v1.2.3