From 13e33e52869d6c863eaa307f9eb5661b6eeeef93 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Mon, 28 Aug 2017 14:57:43 +0100 Subject: coqdoc: Support comments in verbatim output Fixes BZ#5700 --- test-suite/coqdoc/bug5700.html.out | 50 ++++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/bug5700.tex.out | 24 ++++++++++++++++++ test-suite/coqdoc/bug5700.v | 5 ++++ 3 files changed, 79 insertions(+) create mode 100644 test-suite/coqdoc/bug5700.html.out create mode 100644 test-suite/coqdoc/bug5700.tex.out create mode 100644 test-suite/coqdoc/bug5700.v (limited to 'test-suite') diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out new file mode 100644 index 0000000000..0e05660d6c --- /dev/null +++ b/test-suite/coqdoc/bug5700.html.out @@ -0,0 +1,50 @@ + + + + + +Coqdoc.bug5700 + + + + +
+ + + +
+ +

Library Coqdoc.bug5700

+ +
+
+ +
+
foo (* bar *)
+ +
+
+Definition const1 := 1.
+ +
+
+ +
+
more (* nested (* comments *) within verbatim *)
+ +
+
+Definition const2 := 2.
+
+
+ + + +
+ + + \ 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 0000000000..33990cb89f --- /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 0000000000..839034a48f --- /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. -- cgit v1.2.3