From 3d8342c2c26f710583e6b9246bd1069cb8b42d7d Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:10:15 -0400 Subject: [doc] Rewrite and document the prodn directive It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. --- doc/tools/coqrst/coqdomain.py | 136 +++++++++++++++++++++++++----------------- 1 file changed, 81 insertions(+), 55 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index ab3a485b2..c9487abf0 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -28,6 +28,7 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes from sphinx.roles import XRefRole +from sphinx.errors import ExtensionError from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription @@ -103,10 +104,16 @@ class CoqObject(ObjectDescription): 'undocumented': directives.flag } - def _subdomain(self): + def subdomain_data(self): if self.subdomain is None: raise ValueError() - return self.subdomain + return self.env.domaindata['coq']['objects'][self.subdomain] + + def _render_annotation(self, signode): + if self.annotation: + annot_node = nodes.inline(self.annotation, self.annotation, classes=['sigannot']) + signode += addnodes.desc_annotation(self.annotation, '', annot_node) + signode += nodes.Text(' ') def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using @@ -114,29 +121,32 @@ class CoqObject(ObjectDescription): :returns: the name given to the resulting node, if any """ - if self.annotation: - annotation = self.annotation + ' ' - signode += addnodes.desc_annotation(annotation, annotation) + self._render_annotation(signode) self._render_signature(signature, signode) return self._names.get(signature) or self._name_from_signature(signature) + def _warn_if_duplicate_name(self, objects, name): + """Check that two objects in the same domain don't have the same name.""" + if name in objects: + MSG = 'Duplicate object: {}; other is at {}' + msg = MSG.format(name, self.env.doc2path(objects[name][0])) + self.state_machine.reporter.warning(msg, line=self.lineno) + def _record_name(self, name, target_id): """Record a name, mapping it to target_id Warns if another object of the same name already exists. """ - names_in_subdomain = self.env.domaindata['coq']['objects'][self._subdomain()] - # Check that two objects in the same domain don't have the same name - if name in names_in_subdomain: - self.state_machine.reporter.warning( - 'Duplicate Coq object: {}; other is at {}'.format( - name, self.env.doc2path(names_in_subdomain[name][0])), - line=self.lineno) + names_in_subdomain = self.subdomain_data() + self._warn_if_duplicate_name(names_in_subdomain, name) names_in_subdomain[name] = (self.env.docname, self.objtype, target_id) + def _target_id(self, name): + return make_target(self.objtype, nodes.make_id(name)) + def _add_target(self, signode, name): """Register a link target ‘name’, pointing to signode.""" - targetid = make_target(self.objtype, nodes.make_id(name)) + targetid = self._target_id(name) if targetid not in self.state.document.ids: signode['ids'].append(targetid) signode['names'].append(name) @@ -314,50 +324,71 @@ class OptionObject(NotationObject): def _name_from_signature(self, signature): return stringify_with_ellipses(signature) -class ProductionObject(NotationObject): - """Grammar productions. +class ProductionObject(CoqObject): + r"""A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists `_. + + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + """ - # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" - index_suffix = None - annotation = None + #annotation = "Grammar production" - # override to create link targets for production left-hand sides - def run(self): + def _render_signature(self, signature, signode): + raise NotImplementedError(self) + + SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive" + + "\nExpected ``name ::= ...`` or ``name += ...``" + + " (e.g. ``pattern += constr:(@ident)``)") + + def handle_signature(self, signature, signode): + nsplits = 2 + parts = signature.split(maxsplit=nsplits) + if len(parts) != 3: + raise ExtensionError(ProductionObject.SIG_ERROR) + + lhs, op, rhs = (part.strip() for part in parts) + if op not in ["::=", "+="]: + raise ExtensionError(ProductionObject.SIG_ERROR) + + self._render_annotation(signode) + + lhs_op = '{} {} '.format(lhs, op) + lhs_node = nodes.literal(lhs_op, lhs_op) + + position = self.state_machine.get_source_and_line(self.lineno) + rhs_node = parse_notation(rhs, *position) + signode += addnodes.desc_name(signature, '', lhs_node, rhs_node) + + return ('token', lhs) if op == '::=' else None + + def _add_index_entry(self, name, target): + pass + + def _target_id(self, name): + # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around + # https://github.com/sphinx-doc/sphinx/issues/4983 + return 'grammar-token-{}'.format(name[1]) + + def _record_name(self, name, targetid): env = self.state.document.settings.env objects = env.domaindata['std']['objects'] - - class ProdnError(Exception): - """Exception for ill-formed prodn""" - pass - - [idx, node] = super().run() - try: - # find LHS of production - inline_lhs = node[0][0][0][0] # may be fragile !!! - lhs_str = str(inline_lhs) - if lhs_str[0:7] != "