From aee50066c9ef94ec2967e2f6f659ecb7a0f9598e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 25 Jul 2018 15:08:33 +0200 Subject: [sphinx] Add a way of skipping names in the indexes. --- doc/sphinx/README.rst | 2 +- doc/sphinx/README.template.rst | 2 +- doc/tools/coqrst/coqdomain.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 32de15ee31..30ac2cec80 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index f1d2541eb6..c333d6e9d5 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index c9487abf03..8f135c9185 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -158,7 +158,7 @@ class CoqObject(ObjectDescription): def _add_index_entry(self, name, target): """Add `name` (pointing to `target`) to the main index.""" index_text = name - if self.index_suffix: + if self.index_suffix and not name.startswith("_"): index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) -- cgit v1.2.3 From 2bc1ec34aa448278efb53342f17d62743ee245d2 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 25 Jul 2018 11:39:18 -0400 Subject: [sphinx] Do name cleanup in handle_signature --- .../proof-engine/detailed-tactic-examples.rst | 5 ++--- doc/tools/coqrst/coqdomain.py | 21 +++++++++++++-------- 2 files changed, 15 insertions(+), 11 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 78719c1ef1..bb2a8741e2 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -475,9 +475,8 @@ corresponding left-hand side and call yourself recursively on sub- terms. If there is no match, we are at a leaf: return the corresponding constructor (here ``f_const``) applied to the term. -.. exn:: quote: not a simple fixpoint - - Happens when ``quote`` is not able to perform inversion properly. +When ``quote`` is not able to perform inversion properly, it will error out with +:exn:`quote: not a simple fixpoint`. Introducing variables map diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 8f135c9185..610805e8f5 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -123,7 +123,13 @@ class CoqObject(ObjectDescription): """ self._render_annotation(signode) self._render_signature(signature, signode) - return self._names.get(signature) or self._name_from_signature(signature) + name = self._names.get(signature) + if name is None: + name = self._name_from_signature(signature) + # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis) + if name is not None and name.endswith(".") and not name.endswith("..."): + name = name[:-1] + return name def _warn_if_duplicate_name(self, objects, name): """Check that two objects in the same domain don't have the same name.""" @@ -157,18 +163,17 @@ class CoqObject(ObjectDescription): def _add_index_entry(self, name, target): """Add `name` (pointing to `target`) to the main index.""" - index_text = name - if self.index_suffix and not name.startswith("_"): - index_text += " " + self.index_suffix - self.indexnode['entries'].append(('single', index_text, target, '', None)) + assert isinstance(name, str) + if not name.startswith("_"): + index_text = name + if self.index_suffix: + index_text += " " + self.index_suffix + self.indexnode['entries'].append(('single', index_text, target, '', None)) def add_target_and_index(self, name, _, signode): """Attach a link target to `signode` and an index entry for `name`.""" if name: target = self._add_target(signode, name) - # remove trailing . , found in commands, but not ... (ellipsis) - if name[-1] == "." and not name[-3:] == "..." : - name = name[0:-1] self._add_index_entry(name, target) return target -- cgit v1.2.3