diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/_static/notations.css | 5 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 17 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 26 |
3 files changed, 38 insertions, 10 deletions
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index abb08d98cc..e262a9305d 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -267,6 +267,11 @@ code span.error { color: inherit !important; } + +.coqdoc-comment { + color: #808080 !important +} + /* make the error message index readable */ .indextable code { white-space: inherit; /* break long lines */ 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 1428dae7ef..0a9da1dd3e 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'])) |