diff options
| author |  Tej Chajed <tchajed@mit.edu> | 2017-08-28 14:57:43 +0100 |
|---|---|---|
| committer | Tej Chajed <tchajed@mit.edu> | 2017-08-29 09:49:56 +0100 |
| commit | 13e33e52869d6c863eaa307f9eb5661b6eeeef93 (patch) | |
| tree | 1b74bca23d057e8513ba2d8a3088088ee2977155 /test-suite/coqdoc | |
| parent | 7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (diff) | |
coqdoc: Support comments in verbatim output
Fixes BZ#5700
Diffstat (limited to 'test-suite/coqdoc')
| -rw-r--r-- | test-suite/coqdoc/bug5700.html.out | 50 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.tex.out | 24 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.v | 5 |
3 files changed, 79 insertions, 0 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. |