diff options
Diffstat (limited to 'doc/tools/coqrst/coqdomain.py')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 663ab9d37..f09ed4b55 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -108,7 +108,7 @@ class CoqObject(ObjectDescription): annotation = self.annotation + ' ' signode += addnodes.desc_annotation(annotation, annotation) self._render_signature(signature, signode) - return self._name_from_signature(signature) + return self.options.get("name") or self._name_from_signature(signature) @property def _index_suffix(self): @@ -145,14 +145,6 @@ class CoqObject(ObjectDescription): index_text = name + self._index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) - def run(self): - """Small extension of the parent's run method, handling user-provided names.""" - [idx, node] = super().run() - custom_name = self.options.get("name") - if custom_name: - self.add_target_and_index(custom_name, "", node.children[0]) - return [idx, node] - def add_target_and_index(self, name, _, signode): """Create a target and an index entry for name""" if name: @@ -194,13 +186,18 @@ class VernacObject(NotationObject): annotation = "Command" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + m = re.match(r"[a-zA-Z ]+", signature) + if m: + return m.group(0).strip() class VernacVariantObject(VernacObject): """An object to represent variants of Coq commands""" index_suffix = "(cmdv)" annotation = "Variant" + def _name_from_signature(self, signature): + return None + class TacticNotationObject(NotationObject): """An object to represent Coq tactic notations""" subdomain = "tacn" |