diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 43 |
2 files changed, 41 insertions, 4 deletions
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index a004959eb6..cedd60d3bc 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -40,7 +40,7 @@ def coqdoc(coq_code, coqdoc_bin=None): os.write(fd, COQDOC_HEADER.encode("utf-8")) os.write(fd, coq_code.encode("utf-8")) os.close(fd) - return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 2).decode("utf-8") + return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 10).decode("utf-8") finally: os.remove(filename) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 606d725bf0..ab3a485b22 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -97,8 +97,10 @@ class CoqObject(ObjectDescription): raise NotImplementedError(self) option_spec = { - # One can give an explicit name to each documented object - 'name': directives.unchanged + # Explicit object naming + 'name': directives.unchanged, + # Silence warnings produced by report_undocumented_coq_objects + 'undocumented': directives.flag } def _subdomain(self): @@ -116,7 +118,7 @@ class CoqObject(ObjectDescription): annotation = self.annotation + ' ' signode += addnodes.desc_annotation(annotation, annotation) self._render_signature(signature, signode) - return self.options.get("name") or self._name_from_signature(signature) + return self._names.get(signature) or self._name_from_signature(signature) def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -160,6 +162,38 @@ class CoqObject(ObjectDescription): self._add_index_entry(name, target) return target + def _warn_if_undocumented(self): + document = self.state.document + config = document.settings.env.config + report = config.report_undocumented_coq_objects + if report and not self.content and "undocumented" not in self.options: + # This is annoyingly convoluted, but we don't want to raise warnings + # or interrupt the generation of the current node. For more details + # see https://github.com/sphinx-doc/sphinx/issues/4976. + msg = 'No contents in directive {}'.format(self.name) + node = document.reporter.info(msg, line=self.lineno) + getLogger(__name__).info(node.astext()) + if report == "warning": + raise self.warning(msg) + + def _prepare_names(self): + sigs = self.get_signatures() + names = self.options.get("name") + if names is None: + self._names = {} + else: + names = [n.strip() for n in names.split(";")] + if len(names) != len(sigs): + ERR = ("Expected {} semicolon-separated names, got {}. " + + "Please provide one name per signature line.") + raise self.error(ERR.format(len(names), len(sigs))) + self._names = dict(zip(sigs, names)) + + def run(self): + self._warn_if_undocumented() + self._prepare_names() + return super().run() + class PlainObject(CoqObject): """A base class for objects whose signatures should be rendered literally.""" def _render_signature(self, signature, signode): @@ -1036,4 +1070,7 @@ def setup(app): app.add_stylesheet("notations.css") app.add_stylesheet("pre-text.css") + # Tell Sphinx about extra settings + app.add_config_value("report_undocumented_coq_objects", None, 'env') + return {'version': '0.1', "parallel_read_safe": True} |