Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in Sphinx output

Reviewed-by: Zimmi48
Ack-by: cpitclaudel

2 files changed, 33 insertions, 10 deletions

diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index 522b9900a5..51e26a9082 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -28,7 +28,7 @@ from bs4 import BeautifulSoup
 from bs4.element import NavigableString
 
 COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals',
-                  '-s', '--html', '--stdout', '--utf8']
+                  '-s', '--html', '--stdout', '--utf8', '--parse-comments']
 
 COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"]
 COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS)
@@ -68,8 +68,19 @@ def lex(source):
         if isinstance(elem, NavigableString):
             yield [], elem
         elif elem.name == "span":
-            cls = "coqdoc-{}".format(elem['title'])
-            yield [cls], elem.string
+            if elem.string:
+                cls = "coqdoc-{}".format(elem.get("title", "comment"))
+                yield [cls], elem.string
+            else:
+                # handle multi-line comments
+                children = list(elem.children)
+                mlc = children[0].startswith("(*") and children[-1].endswith ("*)")
+                for elem2 in children:
+                    if isinstance(elem2, NavigableString):
+                        cls = ["coqdoc-comment"] if mlc else []
+                        yield cls, elem2
+                    elif elem2.name == 'br':
+                        pass
         elif elem.name == 'br':
             pass
         else:
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index aa95d4f249..468b6b648d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -938,10 +938,11 @@ class CoqtopBlocksTransform(Transform):
 
     @staticmethod
     def split_lines(source):
-        r"""Split Coq input in chunks
+        r"""Split Coq input into chunks, which may include single- or
+        multi-line comments.  Nested comments are not supported.
 
         A chunk is a minimal sequence of consecutive lines of the input that
-        ends with a '.'
+        ends with a '.' or '*)'
 
         >>> split_lines('A.\nB.''')
         ['A.', 'B.']
@@ -962,8 +963,14 @@ class CoqtopBlocksTransform(Transform):
 
         >>> split_lines('SearchHead le.\nSearchHead (@eq bool).')
         ['SearchHead le.', 'SearchHead (@eq bool).']
+
+        >>> split_lines("(* *) x. (* *)\ny.\n")
+        ['(* *) x. (* *)', 'y.']
+
+        >>> split_lines("(* *) x (* \n *)\ny.\n")
+        ['(* *) x (* \n *)', 'y.']
         """
-        return re.split(r"(?<=(?<!\.)\.)\n", source.strip())
+        return re.split(r"(?:(?<=(?<!\.)\.)|(?<=\*\)))\n", source.strip())
 
     @staticmethod
     def parse_options(node):
@@ -1039,7 +1046,11 @@ class CoqtopBlocksTransform(Transform):
         if options['warn']:
             repl.sendone('Set Warnings "default".')
         for sentence in self.split_lines(node.rawsource):
-            pairs.append((sentence, repl.sendone(sentence)))
+            comment = re.compile(r"\s*\(\*.*?\*\)\s*", re.DOTALL)
+            wo_comments = re.sub(comment, "", sentence)
+            has_tac = wo_comments != "" and not wo_comments.isspace()
+            output = repl.sendone(sentence) if has_tac else ""
+            pairs.append((sentence, output))
         if options['abort']:
             repl.sendone('Abort All.')
         if options['fail']:
@@ -1052,9 +1063,10 @@ class CoqtopBlocksTransform(Transform):
             # Use Coqdoc to highlight input
             in_chunks = highlight_using_coqdoc(sentence)
             dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input']))
-            # Parse ANSI sequences to highlight output
-            out_chunks = AnsiColorsParser().colorize_str(output)
-            dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output))
+            if output:
+                # Parse ANSI sequences to highlight output
+                out_chunks = AnsiColorsParser().colorize_str(output)
+                dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output))
         node.clear()
         node.rawsource = self.make_rawsource(pairs, options['input'], options['output'])
         node['classes'].extend(self.block_classes(options['input'] or options['output']))