From ce233d5b4a6f8d506c37a2a492679a66f9618a94 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Wed, 29 Jul 2020 14:53:19 +0200 Subject: coqdoc: Fix the “details” environment The change introduced by 41a1d66 has broken the feature prior to its initial release. We attempt to fix the issue, and add a comment to warn feature developers in order to avoid facing the same issue again. --- doc/changelog/08-tools/12772-fix-details.rst | 5 +++ test-suite/coqdoc/details.html.out | 48 ++++++++++++++++++++++++++++ test-suite/coqdoc/details.tex.out | 44 +++++++++++++++++++++++++ test-suite/coqdoc/details.v | 11 +++++++ tools/coqdoc/cpretty.mll | 6 ++-- 5 files changed, 111 insertions(+), 3 deletions(-) create mode 100644 doc/changelog/08-tools/12772-fix-details.rst create mode 100644 test-suite/coqdoc/details.html.out create mode 100644 test-suite/coqdoc/details.tex.out create mode 100644 test-suite/coqdoc/details.v 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 `_, + 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 @@ + + + + + +Coqdoc.details + + + + +
+ + + +
+ +

Library Coqdoc.details

+ +
+
+
+Definition foo : nat := 3.
+
+
+ +
+
+
Foo bar
+Fixpoint idnat (x : nat) : nat :=
+  match x with
+  | S x ⇒ S (idnat x)
+  | 0 ⇒ 0
+  end.
+
+
+
+
+ + + +
+ + + \ 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; -- cgit v1.2.3