Merge PR #12772: coqdoc: Fix the “details” environment

Reviewed-by: Lysxia
author: Li-yao Xia 2020-08-03 10:50:59 -0400
committer: Li-yao Xia 2020-08-03 10:50:59 -0400
commit: 2793c3cdfd096355270ea02123a7f8fbf64c8076 (patch)
tree: ddac7113d0301ac14dc124c9570de3a89b539051
parent: e0b8b4684eaf76f897ac708ffddbb8e4977ac754 (diff)
parent: ce233d5b4a6f8d506c37a2a492679a66f9618a94 (diff)
5 files changed, 111 insertions, 3 deletions
diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst
new file mode 100644
index 0000000000..67ee061285
--- /dev/null
+++ b/doc/changelog/08-tools/12772-fix-details.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  The `details` environment added in the 8.12 release can now be used
+  as advertised in the reference manual
+  (`#12772 <https://github.com/coq/coq/pull/12772>`_,
+  by Thomas Letan).
diff --git a/test-suite/coqdoc/details.html.out b/test-suite/coqdoc/details.html.out
new file mode 100644
index 0000000000..e1f1ad9867
--- /dev/null
+++ b/test-suite/coqdoc/details.html.out
@@ -0,0 +1,48 @@
+<!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.details</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.details</h1>
+
+<div class="code">
+</div>
+<details><div class="code">
+<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := 3.<br/>
+</div>
+</details><div class="code">
+
+<br/>
+</div>
+<details><summary>Foo bar </summary><div class="code">
+<span class="id" title="keyword">Fixpoint</span> <a id="idnat" class="idref" href="#idnat"><span class="id" title="definition">idnat</span></a> (<a id="x:1" class="idref" href="#x:1"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Coqdoc.details.html#idnat:2"><span class="id" title="definition">idnat</span></a> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a>)<br/>
+&nbsp;&nbsp;| 0 ⇒ 0<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+</div>
+</details><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/details.tex.out b/test-suite/coqdoc/details.tex.out
new file mode 100644
index 0000000000..37778944ba
--- /dev/null
+++ b/test-suite/coqdoc/details.tex.out
@@ -0,0 +1,44 @@
+\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.details}{Library }{Coqdoc.details}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.details.foo}{foo}{\coqdocdefinition{foo}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} := 3.\coqdoceol
+\end{coqdoccode}
+\begin{coqdoccode}
+\coqdocemptyline
+\end{coqdoccode}
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Fixpoint} \coqdef{Coqdoc.details.idnat}{idnat}{\coqdocdefinition{idnat}} (\coqdef{Coqdoc.details.x:1}{x}{\coqdocbinder{x}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} :=\coqdoceol
+\coqdocindent{1.00em}
+\coqdockw{match} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} \coqdocvar{x} \ensuremath{\Rightarrow} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} (\coqref{Coqdoc.details.idnat:2}{\coqdocdefinition{idnat}} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}})\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} 0 \ensuremath{\Rightarrow} 0\coqdoceol
+\coqdocindent{1.00em}
+\coqdockw{end}.\coqdoceol
+\end{coqdoccode}
+\begin{coqdoccode}
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/details.v b/test-suite/coqdoc/details.v
new file mode 100644
index 0000000000..208e60317d
--- /dev/null
+++ b/test-suite/coqdoc/details.v
@@ -0,0 +1,11 @@
+(* begin details *)
+Definition foo : nat := 3.
+(* end details *)
+
+(* begin details : Foo bar *)
+Fixpoint idnat (x : nat) : nat :=
+  match x with
+  | S x => S (idnat x)
+  | 0 => 0
+  end.
+(* end details *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index b801a3b06e..5d210b2e60 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -504,9 +504,9 @@ rule coq_bol = parse
       { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf }
   | space* end_show nl
       { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf }
-  | space* begin_details nl
-      { Lexing.new_line lexbuf;
-        let s = details_body lexbuf in
+  | space* begin_details (* At this point, the comment remains open,
+                            and will be closed by [details_body] *)
+      { let s = details_body lexbuf in
         Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf }
   | space* end_details nl
       { Lexing.new_line lexbuf;
author	Li-yao Xia	2020-08-03 10:50:59 -0400
committer	Li-yao Xia	2020-08-03 10:50:59 -0400
commit	2793c3cdfd096355270ea02123a7f8fbf64c8076 (patch)
tree	ddac7113d0301ac14dc124c9570de3a89b539051
parent	e0b8b4684eaf76f897ac708ffddbb8e4977ac754 (diff)
parent	ce233d5b4a6f8d506c37a2a492679a66f9618a94 (diff)