From 2229ac504ff3b6df7d50eee8b6e3e72c4b52868a Mon Sep 17 00:00:00 2001 From: leo Date: Sat, 13 Dec 2025 23:11:18 +0100 Subject: [PATCH 01/14] uniform numbering option added --- docs/source/conf.py | 2 ++ sphinx_proof/__init__.py | 1 + sphinx_proof/directive.py | 24 ++++++++++++++---------- sphinx_proof/domain.py | 10 +++++----- sphinx_proof/nodes.py | 23 ++++++++++++++--------- 5 files changed, 36 insertions(+), 24 deletions(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index a0347f4..7482cc7 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -56,3 +56,5 @@ # MyST Parser Configuration myst_enable_extensions = ["dollarmath", "amsmath"] + +proof_uniform_numbering = True diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index 61046f3..b5add38 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -81,6 +81,7 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]): def setup(app: Sphinx) -> Dict[str, Any]: app.add_config_value("proof_minimal_theme", False, "html") + app.add_config_value("proof_uniform_numbering", False, "env") app.add_css_file("proof.css") app.connect("build-finished", copy_asset_files) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 9d4595b..06893ae 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -36,13 +36,16 @@ class ElementDirective(SphinxDirective): def run(self) -> List[Node]: env = self.env - typ = self.name.split(":")[1] + realtyp = self.name.split(":")[1] + countertyp = realtyp + if env.config.proof_uniform_numbering: + countertyp = "theorem" serial_no = env.new_serialno() if not hasattr(env, "proof_list"): env.proof_list = {} # If class in options add to class array - classes, class_name = ["proof", typ], self.options.get("class", []) + classes, class_name = ["proof", realtyp], self.options.get("class", []) if class_name: classes.extend(class_name) @@ -53,15 +56,15 @@ def run(self) -> List[Node]: node_id = f"{label}" else: self.options["noindex"] = True - label = f"{typ}-{serial_no}" - node_id = f"{typ}-{serial_no}" + label = f"{realtyp}-{serial_no}" + node_id = f"{realtyp}-{serial_no}" ids = [node_id] # Duplicate label warning if not label == "" and label in env.proof_list.keys(): path = env.doc2path(env.docname)[:-3] other_path = env.doc2path(env.proof_list[label]["docname"]) - msg = f"duplicate {typ} label '{label}', other instance in {other_path}" + msg = f"duplicate {realtyp} label '{label}', other instance in {other_path}" logger.warning(msg, location=path, color="red") title_text = "" @@ -70,13 +73,13 @@ def run(self) -> List[Node]: textnodes, messages = self.state.inline_text(title_text, self.lineno) - section = nodes.section(classes=[f"{typ}-content"], ids=["proof-content"]) + section = nodes.section(classes=[f"{realtyp}-content"], ids=["proof-content"]) self.state.nested_parse(self.content, self.content_offset, section) if "nonumber" in self.options: node = unenumerable_node() else: - node_type = NODE_TYPES[typ] + node_type = NODE_TYPES[countertyp] node = node_type() node.document = self.state.document @@ -88,17 +91,18 @@ def run(self) -> List[Node]: node["classes"].extend(classes) node["title"] = title_text node["label"] = label - node["type"] = typ + node["countertype"] = countertyp + node["realtype"] = realtyp env.proof_list[label] = { "docname": env.docname, - "type": typ, + "countertype": countertyp, + "realtype" : realtyp, "ids": ids, "label": label, "prio": 0, "nonumber": True if "nonumber" in self.options else False, } - return [node] diff --git a/sphinx_proof/domain.py b/sphinx_proof/domain.py index ba8b0ea..a70257e 100644 --- a/sphinx_proof/domain.py +++ b/sphinx_proof/domain.py @@ -45,7 +45,7 @@ def generate(self, docnames=None) -> Tuple[Dict[str, Any], bool]: return content, True proofs = self.domain.env.proof_list - # {'theorem-0': {'docname': 'start/overview', 'type': 'theorem', 'ids': ['theorem-0'], 'label': 'theorem-0', 'prio': 0, 'nonumber': False}} # noqa: E501 + # {'theorem-0': {'docname': 'start/overview', 'realtype': 'theorem', 'countertype': 'theorem', 'ids': ['theorem-0'], 'label': 'theorem-0', 'prio': 0, 'nonumber': False}} # noqa: E501 # name, subtype, docname, typ, anchor, extra, qualifier, description for anchor, values in proofs.items(): @@ -57,7 +57,7 @@ def generate(self, docnames=None) -> Tuple[Dict[str, Any], bool]: anchor, values["docname"], "", - values["type"], + values["realtype"], ) ) @@ -157,11 +157,11 @@ def resolve_xref( if target in contnode[0]: number = "" if not env.proof_list[target]["nonumber"]: - typ = env.proof_list[target]["type"] + countertyp = env.proof_list[target]["countertype"] number = ".".join( - map(str, env.toc_fignumbers[todocname][typ][target]) + map(str, env.toc_fignumbers[todocname][countertyp][target]) ) - title = nodes.Text(f"{translate(match['type'].title())} {number}") + title = nodes.Text(f"{translate(match['countertype'].title())} {number}") # builder, fromdocname, todocname, targetid, child, title=None return make_refnode(builder, fromdocname, todocname, target, title) else: diff --git a/sphinx_proof/nodes.py b/sphinx_proof/nodes.py index 96bbff7..e8faed9 100644 --- a/sphinx_proof/nodes.py +++ b/sphinx_proof/nodes.py @@ -13,6 +13,10 @@ from sphinx.writers.latex import LaTeXTranslator from sphinx.locale import get_translation + +from sphinx.util import logging +logger = logging.getLogger(__name__) + MESSAGE_CATALOG_NAME = "proof" _ = get_translation(MESSAGE_CATALOG_NAME) @@ -31,17 +35,18 @@ def visit_enumerable_node(self, node: Node) -> None: def depart_enumerable_node(self, node: Node) -> None: - typ = node.attributes.get("type", "") + countertyp = node.attributes.get("countertype", "") + realtyp= node.attributes.get("realtype", "") if isinstance(self, LaTeXTranslator): - number = get_node_number(self, node, typ) + number = get_node_number(self, node, countertyp) idx = list_rindex(self.body, latex_admonition_start) + 2 - self.body.insert(idx, f"{typ.title()} {number}") + self.body.insert(idx, f"{realtyp.title()} {number}") self.body.append(latex_admonition_end) else: # Find index in list of 'Proof #' - number = get_node_number(self, node, typ) - idx = self.body.index(f"{typ} {number} ") - self.body[idx] = f"{_(typ.title())} {number} " + number = get_node_number(self, node, countertyp) + idx = self.body.index(f"{countertyp} {number} ") + self.body[idx] = f"{_(realtyp.title())} {number} " self.body.append("") @@ -79,10 +84,10 @@ def depart_proof_node(self, node: Node) -> None: pass -def get_node_number(self, node: Node, typ) -> str: +def get_node_number(self, node: Node, countertyp) -> str: """Get the number for the directive node for HTML.""" ids = node.attributes.get("ids", [])[0] - key = typ + key = countertyp if isinstance(self, LaTeXTranslator): docname = find_parent(self.builder.env, node, "section") fignumbers = self.builder.env.toc_fignumbers.get( @@ -91,7 +96,7 @@ def get_node_number(self, node: Node, typ) -> str: else: fignumbers = self.builder.fignumbers if self.builder.name == "singlehtml": - key = "%s/%s" % (self.docnames[-1], typ) + key = "%s/%s" % (self.docnames[-1], countertyp) number = fignumbers.get(key, {}).get(ids, ()) return ".".join(map(str, number)) From 0ab56b91f096e9d03ac62286c31943a22d975140 Mon Sep 17 00:00:00 2001 From: leo Date: Sat, 13 Dec 2025 23:21:09 +0100 Subject: [PATCH 02/14] fixed tests --- sphinx_proof/directive.py | 8 ++++---- sphinx_proof/nodes.py | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 06893ae..237b175 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -119,16 +119,16 @@ class ProofDirective(SphinxDirective): } def run(self) -> List[Node]: - typ = self.name.split(":")[1] + realtyp = self.name.split(":")[1] # If class in options add to class array - classes, class_name = ["proof", typ], self.options.get("class", []) + classes, class_name = ["proof", realtyp], self.options.get("class", []) if class_name: classes.extend(class_name) - section = nodes.admonition(classes=classes, ids=[typ]) + section = nodes.admonition(classes=classes, ids=[realtyp]) - self.content[0] = "{}. ".format(typ.title()) + self.content[0] + self.content[0] = "{}. ".format(realtyp.title()) + self.content[0] self.state.nested_parse(self.content, 0, section) node = proof_node() diff --git a/sphinx_proof/nodes.py b/sphinx_proof/nodes.py index e8faed9..610ed5f 100644 --- a/sphinx_proof/nodes.py +++ b/sphinx_proof/nodes.py @@ -60,18 +60,18 @@ def visit_unenumerable_node(self, node: Node) -> None: def depart_unenumerable_node(self, node: Node) -> None: - typ = node.attributes.get("type", "") + realtyp = node.attributes.get("realtype", "") title = node.attributes.get("title", "") if isinstance(self, LaTeXTranslator): idx = list_rindex(self.body, latex_admonition_start) + 2 - self.body.insert(idx, f"{typ.title()}") + self.body.insert(idx, f"{realtyp.title()}") self.body.append(latex_admonition_end) else: if title == "": idx = list_rindex(self.body, '

') + 1 else: idx = list_rindex(self.body, title) - element = f"{_(typ.title())} " + element = f"{_(realtyp.title())} " self.body.insert(idx, element) self.body.append("") From bbae3d259fdbf7fe7f0c2dd9c8f185ab1a50c790 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 13 Dec 2025 22:30:45 +0000 Subject: [PATCH 03/14] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- sphinx_proof/directive.py | 2 +- sphinx_proof/domain.py | 4 +++- sphinx_proof/nodes.py | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 237b175..334b6aa 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -97,7 +97,7 @@ def run(self) -> List[Node]: env.proof_list[label] = { "docname": env.docname, "countertype": countertyp, - "realtype" : realtyp, + "realtype": realtyp, "ids": ids, "label": label, "prio": 0, diff --git a/sphinx_proof/domain.py b/sphinx_proof/domain.py index a70257e..40537e3 100644 --- a/sphinx_proof/domain.py +++ b/sphinx_proof/domain.py @@ -161,7 +161,9 @@ def resolve_xref( number = ".".join( map(str, env.toc_fignumbers[todocname][countertyp][target]) ) - title = nodes.Text(f"{translate(match['countertype'].title())} {number}") + title = nodes.Text( + f"{translate(match['countertype'].title())} {number}" + ) # builder, fromdocname, todocname, targetid, child, title=None return make_refnode(builder, fromdocname, todocname, target, title) else: diff --git a/sphinx_proof/nodes.py b/sphinx_proof/nodes.py index 610ed5f..76977e4 100644 --- a/sphinx_proof/nodes.py +++ b/sphinx_proof/nodes.py @@ -15,6 +15,7 @@ from sphinx.util import logging + logger = logging.getLogger(__name__) MESSAGE_CATALOG_NAME = "proof" @@ -36,7 +37,7 @@ def visit_enumerable_node(self, node: Node) -> None: def depart_enumerable_node(self, node: Node) -> None: countertyp = node.attributes.get("countertype", "") - realtyp= node.attributes.get("realtype", "") + realtyp = node.attributes.get("realtype", "") if isinstance(self, LaTeXTranslator): number = get_node_number(self, node, countertyp) idx = list_rindex(self.body, latex_admonition_start) + 2 From 770f0e9a801883b7162ae6d9e79b91d2041c61b2 Mon Sep 17 00:00:00 2001 From: leo Date: Sat, 13 Dec 2025 23:46:56 +0100 Subject: [PATCH 04/14] doc added --- docs/source/options.md | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/docs/source/options.md b/docs/source/options.md index 6433d49..366607d 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -1,5 +1,7 @@ # Options +## Minimal color scheme + This package has the option to choose a more **minimal** color scheme. The aim is to create admonitions that are clearly different to the core text with @@ -15,7 +17,7 @@ compared to the current default To enable the `minimal` color scheme you can use the following. -## Jupyter Book Project +### Jupyter Book Project Add `proof_minimal_theme = True` to your `_config.yml` @@ -25,6 +27,27 @@ sphinx: proof_minimal_theme: true ``` -## Sphinx Project +### Sphinx Project Add `proof_minimal_theme = True` to your `conf.py` + + +## Shared numbering + +By default, each type of theorem has their own numbering and counter. +This can be changed to a common counter by setting the option `proof_uniform_numbering` to true. + +### Sphinx Project + +Add `proof_uniform_numbering = True` to your `conf.py` + + +### Jupyter Book Project + +Add `proof_uniform_numbering = True` to your `_config.yml` (untested) + +```yaml +sphinx: + config: + proof_uniform_numbering: true +``` From 7b251073c590be4722ac31ff88a8e1487ff446b3 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 13 Dec 2025 22:47:07 +0000 Subject: [PATCH 05/14] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- docs/source/options.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/options.md b/docs/source/options.md index 366607d..8d9c083 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -32,7 +32,7 @@ sphinx: Add `proof_minimal_theme = True` to your `conf.py` -## Shared numbering +## Shared numbering By default, each type of theorem has their own numbering and counter. This can be changed to a common counter by setting the option `proof_uniform_numbering` to true. From fe5544b4b18c4e47647e949113776c9fda7291e7 Mon Sep 17 00:00:00 2001 From: leo Date: Sun, 14 Dec 2025 00:02:11 +0100 Subject: [PATCH 06/14] reference label corrected --- sphinx_proof/domain.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sphinx_proof/domain.py b/sphinx_proof/domain.py index 40537e3..01be94f 100644 --- a/sphinx_proof/domain.py +++ b/sphinx_proof/domain.py @@ -162,7 +162,7 @@ def resolve_xref( map(str, env.toc_fignumbers[todocname][countertyp][target]) ) title = nodes.Text( - f"{translate(match['countertype'].title())} {number}" + f"{translate(match["realtype"].title())} {number}" ) # builder, fromdocname, todocname, targetid, child, title=None return make_refnode(builder, fromdocname, todocname, target, title) From 91b83dd705ee6361d5b969fbc42de4395875850f Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 13 Dec 2025 23:02:20 +0000 Subject: [PATCH 07/14] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- sphinx_proof/domain.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/sphinx_proof/domain.py b/sphinx_proof/domain.py index 01be94f..d9d8a06 100644 --- a/sphinx_proof/domain.py +++ b/sphinx_proof/domain.py @@ -161,9 +161,7 @@ def resolve_xref( number = ".".join( map(str, env.toc_fignumbers[todocname][countertyp][target]) ) - title = nodes.Text( - f"{translate(match["realtype"].title())} {number}" - ) + title = nodes.Text(f"{translate(match["realtype"].title())} {number}") # builder, fromdocname, todocname, targetid, child, title=None return make_refnode(builder, fromdocname, todocname, target, title) else: From 65a9d21ae573293db8d760bbb1cc65c7fafcee3b Mon Sep 17 00:00:00 2001 From: leo Date: Tue, 20 Jan 2026 17:52:51 +0100 Subject: [PATCH 08/14] made numbering fully customizable --- docs/source/conf.py | 18 +++++++++++++++++- docs/source/options.md | 30 +++++++++++++++++++++--------- sphinx_proof/__init__.py | 23 ++++++++++++++++++++++- sphinx_proof/directive.py | 4 +--- 4 files changed, 61 insertions(+), 14 deletions(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index 7482cc7..3bc72ab 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -57,4 +57,20 @@ myst_enable_extensions = ["dollarmath", "amsmath"] -proof_uniform_numbering = True +prf_realtyp_to_countertyp = { + "axiom": "theorem", + "theorem": "theorem", + "lemma": "theorem", + "algorithm": "theorem", + "definition": "theorem", + "remark": "theorem", + "conjecture": "theorem", + "corollary": "theorem", + "criterion": "theorem", + "example": "theorem", + "property": "theorem", + "observation": "theorem", + "proposition": "theorem", + "assumption": "theorem", + "notation": "theorem", +} diff --git a/docs/source/options.md b/docs/source/options.md index 8d9c083..5475386 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -35,19 +35,31 @@ Add `proof_minimal_theme = True` to your `conf.py` ## Shared numbering By default, each type of theorem has their own numbering and counter. -This can be changed to a common counter by setting the option `proof_uniform_numbering` to true. +This can be changed to a common counter by setting the option `prf_realtyp_to_countertyp` to a dictionary associating to each prf-type which prf-type's counter it should use. ### Sphinx Project -Add `proof_uniform_numbering = True` to your `conf.py` +In `conf.py`, e.g. to have a shared counter for all prf-types: +``` +prf_realtyp_to_countertyp = { + "axiom": "theorem", + "theorem": "theorem", + "lemma": "theorem", + "algorithm": "theorem", + "definition": "theorem", + "remark": "theorem", + "conjecture": "theorem", + "corollary": "theorem", + "criterion": "theorem", + "example": "theorem", + "property": "theorem", + "observation": "theorem", + "proposition": "theorem", + "assumption": "theorem", + "notation": "theorem", +} +``` -### Jupyter Book Project -Add `proof_uniform_numbering = True` to your `_config.yml` (untested) -```yaml -sphinx: - config: - proof_uniform_numbering: true -``` diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index b5add38..667f41f 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -78,10 +78,31 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]): copy_asset(path, str(Path(app.outdir).joinpath("_static").absolute())) + +realtyp_to_countertyp = { + "axiom": "axiom", + "theorem": "theorem", + "lemma": "lemma", + "algorithm": "algorithm", + "definition": "definition", + "remark": "remark", + "conjecture": "conjecture", + "corollary": "corollary", + "criterion": "criterion", + "example": "example", + "property": "property", + "observation": "observation", + "proposition": "proposition", + "assumption": "assumption", + "notation": "notation", +} + + + def setup(app: Sphinx) -> Dict[str, Any]: app.add_config_value("proof_minimal_theme", False, "html") - app.add_config_value("proof_uniform_numbering", False, "env") + app.add_config_value("prf_realtyp_to_countertyp", realtyp_to_countertyp, "env") app.add_css_file("proof.css") app.connect("build-finished", copy_asset_files) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 334b6aa..2b30678 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -37,9 +37,7 @@ class ElementDirective(SphinxDirective): def run(self) -> List[Node]: env = self.env realtyp = self.name.split(":")[1] - countertyp = realtyp - if env.config.proof_uniform_numbering: - countertyp = "theorem" + countertyp = env.config.prf_realtyp_to_countertyp[realtyp] serial_no = env.new_serialno() if not hasattr(env, "proof_list"): env.proof_list = {} From 3c334bd85d65a8675d8c8c5334b81340699a5902 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Tue, 20 Jan 2026 16:53:02 +0000 Subject: [PATCH 09/14] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- docs/source/options.md | 3 --- sphinx_proof/__init__.py | 2 -- 2 files changed, 5 deletions(-) diff --git a/docs/source/options.md b/docs/source/options.md index 5475386..51e3311 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -60,6 +60,3 @@ prf_realtyp_to_countertyp = { "notation": "theorem", } ``` - - - diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index 667f41f..f0f4f30 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -78,7 +78,6 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]): copy_asset(path, str(Path(app.outdir).joinpath("_static").absolute())) - realtyp_to_countertyp = { "axiom": "axiom", "theorem": "theorem", @@ -98,7 +97,6 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]): } - def setup(app: Sphinx) -> Dict[str, Any]: app.add_config_value("proof_minimal_theme", False, "html") From c93d1bf555322791d1f7e96420b6742aabf279cb Mon Sep 17 00:00:00 2001 From: leo Date: Wed, 21 Jan 2026 19:23:51 +0100 Subject: [PATCH 10/14] partial remapping now possible --- docs/source/conf.py | 18 +----------------- docs/source/options.md | 2 +- sphinx_proof/__init__.py | 20 +------------------- sphinx_proof/directive.py | 23 ++++++++++++++++++++++- 4 files changed, 25 insertions(+), 38 deletions(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index 3bc72ab..1d89a4f 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -57,20 +57,4 @@ myst_enable_extensions = ["dollarmath", "amsmath"] -prf_realtyp_to_countertyp = { - "axiom": "theorem", - "theorem": "theorem", - "lemma": "theorem", - "algorithm": "theorem", - "definition": "theorem", - "remark": "theorem", - "conjecture": "theorem", - "corollary": "theorem", - "criterion": "theorem", - "example": "theorem", - "property": "theorem", - "observation": "theorem", - "proposition": "theorem", - "assumption": "theorem", - "notation": "theorem", -} +prf_realtyp_to_countertyp = {} diff --git a/docs/source/options.md b/docs/source/options.md index 51e3311..eee0df8 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -35,7 +35,7 @@ Add `proof_minimal_theme = True` to your `conf.py` ## Shared numbering By default, each type of theorem has their own numbering and counter. -This can be changed to a common counter by setting the option `prf_realtyp_to_countertyp` to a dictionary associating to each prf-type which prf-type's counter it should use. +This can be changed by setting the option `prf_realtyp_to_countertyp` to a dictionary associating to a prf-type which prf-type's counter it should use. ### Sphinx Project diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index f0f4f30..83be3a8 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -78,29 +78,11 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]): copy_asset(path, str(Path(app.outdir).joinpath("_static").absolute())) -realtyp_to_countertyp = { - "axiom": "axiom", - "theorem": "theorem", - "lemma": "lemma", - "algorithm": "algorithm", - "definition": "definition", - "remark": "remark", - "conjecture": "conjecture", - "corollary": "corollary", - "criterion": "criterion", - "example": "example", - "property": "property", - "observation": "observation", - "proposition": "proposition", - "assumption": "assumption", - "notation": "notation", -} - def setup(app: Sphinx) -> Dict[str, Any]: app.add_config_value("proof_minimal_theme", False, "html") - app.add_config_value("prf_realtyp_to_countertyp", realtyp_to_countertyp, "env") + app.add_config_value("prf_realtyp_to_countertyp", {}, "env") app.add_css_file("proof.css") app.connect("build-finished", copy_asset_files) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 2b30678..e38c2a9 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -20,6 +20,27 @@ logger = logging.getLogger(__name__) + +DEFAULT_REALTYP_TO_COUNTERTYP = { + "axiom": "axiom", + "theorem": "theorem", + "lemma": "lemma", + "algorithm": "algorithm", + "definition": "definition", + "remark": "remark", + "conjecture": "conjecture", + "corollary": "corollary", + "criterion": "criterion", + "example": "example", + "property": "property", + "observation": "observation", + "proposition": "proposition", + "assumption": "assumption", + "notation": "notation", +} + + + class ElementDirective(SphinxDirective): """A custom Sphinx Directive""" @@ -37,7 +58,7 @@ class ElementDirective(SphinxDirective): def run(self) -> List[Node]: env = self.env realtyp = self.name.split(":")[1] - countertyp = env.config.prf_realtyp_to_countertyp[realtyp] + countertyp = env.config.prf_realtyp_to_countertyp.get(realtyp, DEFAULT_REALTYP_TO_COUNTERTYP[realtyp]) serial_no = env.new_serialno() if not hasattr(env, "proof_list"): env.proof_list = {} From e4902b35108797982bb225df8efd4f0d8650da9e Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Wed, 21 Jan 2026 18:24:06 +0000 Subject: [PATCH 11/14] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- sphinx_proof/__init__.py | 1 - sphinx_proof/directive.py | 6 +++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index 83be3a8..44834a8 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -78,7 +78,6 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]): copy_asset(path, str(Path(app.outdir).joinpath("_static").absolute())) - def setup(app: Sphinx) -> Dict[str, Any]: app.add_config_value("proof_minimal_theme", False, "html") diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index e38c2a9..8441aa1 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -20,7 +20,6 @@ logger = logging.getLogger(__name__) - DEFAULT_REALTYP_TO_COUNTERTYP = { "axiom": "axiom", "theorem": "theorem", @@ -40,7 +39,6 @@ } - class ElementDirective(SphinxDirective): """A custom Sphinx Directive""" @@ -58,7 +56,9 @@ class ElementDirective(SphinxDirective): def run(self) -> List[Node]: env = self.env realtyp = self.name.split(":")[1] - countertyp = env.config.prf_realtyp_to_countertyp.get(realtyp, DEFAULT_REALTYP_TO_COUNTERTYP[realtyp]) + countertyp = env.config.prf_realtyp_to_countertyp.get( + realtyp, DEFAULT_REALTYP_TO_COUNTERTYP[realtyp] + ) serial_no = env.new_serialno() if not hasattr(env, "proof_list"): env.proof_list = {} From 95a01a9fbe9fe91efdb48b3863faa96d8c736a69 Mon Sep 17 00:00:00 2001 From: leo Date: Wed, 21 Jan 2026 22:00:31 +0100 Subject: [PATCH 12/14] improved doc --- docs/source/options.md | 31 ++++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/docs/source/options.md b/docs/source/options.md index eee0df8..e1b5d57 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -34,12 +34,11 @@ Add `proof_minimal_theme = True` to your `conf.py` ## Shared numbering -By default, each type of theorem has their own numbering and counter. -This can be changed by setting the option `prf_realtyp_to_countertyp` to a dictionary associating to a prf-type which prf-type's counter it should use. +By default, each type of (prf-)directive has their own numbering and counter. This can be changed by setting the option `prf_realtyp_to_countertyp` to a dictionary associating to a directive which the counter of which directive it should use. ### Sphinx Project -In `conf.py`, e.g. to have a shared counter for all prf-types: +In `conf.py`, e.g. to have a shared counter for all directives: ``` prf_realtyp_to_countertyp = { @@ -60,3 +59,29 @@ prf_realtyp_to_countertyp = { "notation": "theorem", } ``` + +In the following case, the directives `lemma`, `conjecture`, `corollary` and `proposition` will share the counter with `theorem`, while `axiom` and `assumption` will share the counter with `definition`. All other directives would use their original counter. + + +``` +prf_realtyp_to_countertyp = { + "lemma": "theorem", + "conjecture": "theorem", + "corollary": "theorem", + "proposition": "theorem", + "axiom": "definition", + "assumption": "definition", +} +``` + +````{warning} +The association of a counter to a directive is not transitive: Let us consider the following configuration: +``` +prf_realtyp_to_countertyp = { + "lemma": "theorem", + "conjecture": "lemma", +} +``` +The `lemma` and `theorem` directives share a counter, however the `conjecture` directive has a separate counter (the `lemma` counter which is **not** used by `lemma` directives). +```` + From 2f493b31152fe580b0a61fbbfd87b476b9a49bba Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Wed, 21 Jan 2026 21:01:50 +0000 Subject: [PATCH 13/14] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- docs/source/options.md | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/source/options.md b/docs/source/options.md index e1b5d57..6de9c0b 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -84,4 +84,3 @@ prf_realtyp_to_countertyp = { ``` The `lemma` and `theorem` directives share a counter, however the `conjecture` directive has a separate counter (the `lemma` counter which is **not** used by `lemma` directives). ```` - From 86225f8dbd3ecc51b6a0af52a0a99df2019a0082 Mon Sep 17 00:00:00 2001 From: leo Date: Fri, 23 Jan 2026 20:38:20 +0100 Subject: [PATCH 14/14] changed env to html and added newline in docs --- docs/source/options.md | 2 ++ sphinx_proof/__init__.py | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/source/options.md b/docs/source/options.md index 6de9c0b..2863260 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -76,11 +76,13 @@ prf_realtyp_to_countertyp = { ````{warning} The association of a counter to a directive is not transitive: Let us consider the following configuration: + ``` prf_realtyp_to_countertyp = { "lemma": "theorem", "conjecture": "lemma", } ``` + The `lemma` and `theorem` directives share a counter, however the `conjecture` directive has a separate counter (the `lemma` counter which is **not** used by `lemma` directives). ```` diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index 44834a8..7e34414 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -81,7 +81,7 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]): def setup(app: Sphinx) -> Dict[str, Any]: app.add_config_value("proof_minimal_theme", False, "html") - app.add_config_value("prf_realtyp_to_countertyp", {}, "env") + app.add_config_value("prf_realtyp_to_countertyp", {}, "html") app.add_css_file("proof.css") app.connect("build-finished", copy_asset_files)