aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-14 21:57:53 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-14 21:59:15 +0200
commitab2e6772c6cbe2e6fa8851a1b399222a2a7740e3 (patch)
tree8bd8a4bd811af8a57f7b675741221a5a9c849511 /doc/tools
parent3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (diff)
[Sphinx] Fix all remaining warnings.
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/coqrst/coqdomain.py17
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"