diff options
| author | Clément Pit-Claudel | 2018-05-17 22:28:19 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | 48662f95c63a02d90630941aace96e7b44dcc247 (patch) | |
| tree | 8fe9c02c543998695f5c7238dffd049d21cf1b1c | |
| parent | a5586852cca4a8a9b57506fd2ea09438bd5bda2e (diff) | |
[doc] Ensure that merging coqtop blocks preserves anchors
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 86f5622912..1ae2a4a19f 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -846,23 +846,28 @@ class CoqtopBlocksTransform(Transform): kept_node['classes'] = [c for c in kept_node['classes'] if c != 'coqtop-hidden'] - def merge_consecutive_coqtop_blocks(self): + @staticmethod + def merge_consecutive_coqtop_blocks(app, doctree, _): """Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate.""" - for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): + for node in doctree.traverse(CoqtopBlocksTransform.is_coqtop_block): if node.parent: + rawsources, names = [node.rawsource], set(node['names']) for sibling in node.traverse(include_self=False, descend=False, siblings=True, ascend=False): if CoqtopBlocksTransform.is_coqtop_block(sibling): - self.merge_coqtop_classes(node, sibling) + CoqtopBlocksTransform.merge_coqtop_classes(node, sibling) + rawsources.append(sibling.rawsource) + names.update(sibling['names']) node.extend(sibling.children) node.parent.remove(sibling) sibling.parent = None else: break + node.rawsource = "\n\n".join(rawsources) + node['names'] = list(names) def apply(self): self.add_coqtop_output() - self.merge_consecutive_coqtop_blocks() class CoqSubdomainsIndex(Index): """Index subclass to provide subdomain-specific indices. @@ -1078,7 +1083,6 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: pygments if available. This prevents the LaTeX builder from getting confused. """ - is_html = app.builder.tags.has("html") for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: @@ -1115,6 +1119,7 @@ def setup(app): app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) + app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles app.add_stylesheet("fonts.css") |