coqdoc: Add (* begin details *) and (* end details *)

We propose to add an environment to have foldable texts with HTML
output, more precisely:

    (*begin details [: An optional summary] *)

    some Coq and documentation material

    (* end details *)

Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.

5 files changed, 76 insertions, 0 deletions

diff --git a/doc/changelog/08-tools/10592-coqdoc-details.rst b/doc/changelog/08-tools/10592-coqdoc-details.rst
new file mode 100644
index 0000000000..c5bdc1dbb0
--- /dev/null
+++ b/doc/changelog/08-tools/10592-coqdoc-details.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  A new documentation environment ``details`` to make certain portion
+  of a Coq document foldable.  See :ref:`coqdoc`
+  (`#10592 <https://github.com/coq/coq/pull/10592>`_,
+  by Thomas Letan).
diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index cada680895..b4b14fb392 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -248,6 +248,27 @@ shown using such comments:
 The latter cannot be used around some inner parts of a proof, but can
 be used around a whole proof.
 
+Lastly, it is possible to adopt a middle-ground approach when the
+desired output is HTML, where a given snippet of Coq material is
+hidden by default, but can be made visible with user interaction.
+
+::
+
+
+    (* begin details *)
+     *some Coq material*
+    (* end details *)
+
+
+There is also an alternative syntax available.
+
+::
+
+
+    (* begin details : Some summary describing the snippet *)
+     *some Coq material*
+    (* end details *)
+
 
 Usage
 ~~~~~
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 210ac754a1..0f25bc8e12 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -116,6 +116,11 @@
   let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
   let end_show () = restore_state ()
 
+  let begin_details s =
+    save_state (); Cdglobals.gallina := false; Cdglobals.light := false;
+    Output.start_details s
+  let end_details () = Output.stop_details (); restore_state ()
+
   (* Reset the globals *)
 
   let reset () =
@@ -434,6 +439,8 @@ let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
 let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
 let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
 let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
+let begin_details = "(*" space* "begin" space+ "details" space*
+let end_details = "(*" space* "end" space+ "details" space* "*)" space* nl
 (*
 let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
 let end_verb = "(*" space* "end" space+ "verb" space* "*)"
@@ -460,6 +467,11 @@ rule coq_bol = parse
       { begin_show (); coq_bol lexbuf }
   | space* end_show
       { end_show (); coq_bol lexbuf }
+  | space* begin_details
+      { let s = details_body lexbuf in
+        Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf }
+  | space* end_details
+      { Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf }
   | space* (("Local"|"Global") space+)? gallina_kw_to_hide
       { let s = lexeme lexbuf in
 	  if !Cdglobals.light && section_or_end s then
@@ -1221,6 +1233,19 @@ and printing_token_body = parse
   | _   { Buffer.add_string token_buffer (lexeme lexbuf);
 	  printing_token_body lexbuf }
 
+and details_body = parse
+  | "*)" space* nl? | eof
+        { None }
+  | ":" space*  { details_body_rec lexbuf }
+
+and details_body_rec = parse
+  | "*)" space* nl? | eof
+        { let s = Buffer.contents token_buffer in
+          Buffer.clear token_buffer;
+          Some s }
+  | _   { Buffer.add_string token_buffer (lexeme lexbuf);
+          details_body_rec lexbuf }
+
 (*s These handle inference rules, parsing the body segments of things
     enclosed in [[[  ]]] brackets *)
 and inf_rules indents = parse
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index d2b0078a7c..7a70a92ba8 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -469,6 +469,11 @@ module Latex = struct
 
   let stop_emph () = printf "}"
 
+  let start_details _ = ()
+
+  let stop_details () = ()
+
+
   let start_comment () = printf "\\begin{coqdoccomment}\n"
 
   let end_comment () = printf "\\end{coqdoccomment}\n"
@@ -740,6 +745,12 @@ module Html = struct
 
   let stop_emph () = printf "</i>"
 
+  let start_details = function
+    | Some s -> printf "<details><summary>%s</summary>" s
+    | _ -> printf "<details>"
+
+  let stop_details () = printf "</details>"
+
   let start_comment () = printf "<span class=\"comment\">(*"
 
   let end_comment () = printf "*)</span>"
@@ -1053,6 +1064,9 @@ module TeXmacs = struct
   let start_emph () = printf "<with|font shape|italic|"
   let stop_emph () = printf ">"
 
+  let start_details _ = ()
+  let stop_details () = ()
+
   let start_comment () = ()
   let end_comment () = ()
 
@@ -1159,6 +1173,9 @@ module Raw = struct
   let start_emph () = printf "_"
   let stop_emph () = printf "_"
 
+  let start_details _ = ()
+  let stop_details () = ()
+
   let start_comment () = printf "(*"
   let end_comment () = printf "*)"
 
@@ -1272,6 +1289,11 @@ let start_emph =
 let stop_emph =
   select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph
 
+let start_details =
+  select Latex.start_details Html.start_details TeXmacs.start_details Raw.start_details
+let stop_details =
+  select Latex.stop_details Html.stop_details TeXmacs.stop_details Raw.stop_details
+
 let start_latex_math =
   select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
 let stop_latex_math =
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 485183a4ed..b7a8d4d858 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -29,6 +29,9 @@ val start_module : unit -> unit
 val start_doc : unit -> unit
 val end_doc : unit -> unit
 
+val start_details : string option -> unit
+val stop_details : unit -> unit
+
 val start_emph : unit -> unit
 val stop_emph : unit -> unit