diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 65 |
1 files changed, 56 insertions, 9 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 2bf9776751..edf4e6ec9d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -333,15 +333,15 @@ class TacticNotationVariantObject(TacticNotationObject): annotation = "Variant" class OptionObject(NotationObject): - """A Coq option. + """A Coq option (a setting with non-boolean value, e.g. a string or numeric value). Example:: - .. opt:: Nonrecursive Elimination Schemes + .. opt:: Hyps Limit @num + :name Hyps Limit - This option controls whether types declared with the keywords - :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the - induction principles. + Controls the maximum number of hypotheses displayed in goals after + application of a tactic. """ subdomain = "opt" index_suffix = "(opt)" @@ -350,6 +350,43 @@ class OptionObject(NotationObject): def _name_from_signature(self, signature): return stringify_with_ellipses(signature) + +class FlagObject(NotationObject): + """A Coq flag (i.e. a boolean setting). + + Example:: + + .. flag:: Nonrecursive Elimination Schemes + + Controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of + induction principles. + """ + subdomain = "flag" + index_suffix = "(flag)" + annotation = "Flag" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + + +class TableObject(NotationObject): + """A Coq table, i.e. a setting that is a set of values. + + Example:: + + .. table:: Search Blacklist @string + :name: Search Blacklist + + Controls ... + """ + subdomain = "table" + index_suffix = "(table)" + annotation = "Table" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + class ProductionObject(CoqObject): r"""A grammar production. @@ -629,7 +666,9 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(Directive): r"""A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + contents of the TeX file are wrapped in a math environment, as MathJax + doesn't process LaTeX definitions otherwise. Usage:: @@ -656,7 +695,7 @@ class PreambleDirective(Directive): with open(abs_fname, encoding="utf-8") as ltx: latex = ltx.read() - node = make_math_node(latex, env.docname, nowrap=True) + node = make_math_node(latex, env.docname, nowrap=False) node['classes'] = ["math-preamble"] set_source_info(self, node) return [node] @@ -912,7 +951,7 @@ class CoqTacticIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"] class CoqOptionIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] + name, localname, shortname, subdomains = "optindex", "Flags, options and Tables Index", "options", ["flag", "opt", "table"] class CoqGallinaIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"] @@ -985,6 +1024,8 @@ class CoqDomain(Domain): 'tacn': ObjType('tacn', 'tacn'), 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), + 'flag': ObjType('flag', 'flag'), + 'table': ObjType('table', 'table'), 'thm': ObjType('thm', 'thm'), 'prodn': ObjType('prodn', 'prodn'), 'exn': ObjType('exn', 'exn'), @@ -1001,6 +1042,8 @@ class CoqDomain(Domain): 'tacn': TacticNotationObject, 'tacv': TacticNotationVariantObject, 'opt': OptionObject, + 'flag': FlagObject, + 'table': TableObject, 'thm': GallinaObject, 'prodn' : ProductionObject, 'exn': ExceptionObject, @@ -1012,6 +1055,8 @@ class CoqDomain(Domain): 'cmd': XRefRole(warn_dangling=True), 'tacn': XRefRole(warn_dangling=True), 'opt': XRefRole(warn_dangling=True), + 'flag': XRefRole(warn_dangling=True), + 'table': XRefRole(warn_dangling=True), 'thm': XRefRole(warn_dangling=True), 'prodn' : XRefRole(warn_dangling=True), 'exn': XRefRole(warn_dangling=True), @@ -1033,6 +1078,8 @@ class CoqDomain(Domain): 'cmd': {}, 'tacn': {}, 'opt': {}, + 'flag': {}, + 'table': {}, 'thm': {}, 'prodn' : {}, 'exn': {}, @@ -1149,6 +1196,6 @@ def setup(app): # contents of ``env.domaindata['coq']`` change. See # `https://github.com/sphinx-doc/sphinx/issues/4460`. meta = { "version": "0.1", - "env_version": 1, + "env_version": 2, "parallel_read_safe": True } return meta |