From cb49b2ae21f99566cda6eb73bcce7901b5b505f1 Mon Sep 17 00:00:00 2001 From: Leonid Ryvkin Date: Sat, 24 Jan 2026 22:00:43 +0100 Subject: [PATCH 01/10] feat: Added possibility for shared numbering of theorems, fixing issue #64 (#161) Added optioin to have directives share numbering. Reflected also in docs. --- docs/source/conf.py | 2 ++ docs/source/options.md | 62 +++++++++++++++++++++++++++++++++++++-- sphinx_proof/__init__.py | 1 + sphinx_proof/directive.py | 51 +++++++++++++++++++++++--------- sphinx_proof/domain.py | 10 +++---- sphinx_proof/nodes.py | 30 +++++++++++-------- 6 files changed, 123 insertions(+), 33 deletions(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index a0347f4..1d89a4f 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -56,3 +56,5 @@ # MyST Parser Configuration myst_enable_extensions = ["dollarmath", "amsmath"] + +prf_realtyp_to_countertyp = {} diff --git a/docs/source/options.md b/docs/source/options.md index 6433d49..2863260 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,62 @@ 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 (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 directives: + +``` +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", +} +``` + +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). +```` diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index 61046f3..7e34414 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("prf_realtyp_to_countertyp", {}, "html") 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..8441aa1 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -20,6 +20,25 @@ 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""" @@ -36,13 +55,16 @@ class ElementDirective(SphinxDirective): def run(self) -> List[Node]: env = self.env - typ = self.name.split(":")[1] + realtyp = self.name.split(":")[1] + 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 = {} # 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 +75,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 +92,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 +110,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] @@ -115,16 +138,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/domain.py b/sphinx_proof/domain.py index ba8b0ea..d9d8a06 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["realtype"].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..76977e4 100644 --- a/sphinx_proof/nodes.py +++ b/sphinx_proof/nodes.py @@ -13,6 +13,11 @@ 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 +36,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("") @@ -55,18 +61,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("") @@ -79,10 +85,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 +97,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 b14d019ca5773797f5f27ddb7faad16bc4bc12d4 Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 22:09:24 +0100 Subject: [PATCH 02/10] Refactor title creation in ProofDomain Extracted the translated type title into a separate variable for clarity before constructing the title node in ProofDomain. --- sphinx_proof/domain.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/sphinx_proof/domain.py b/sphinx_proof/domain.py index d9d8a06..7558a0f 100644 --- a/sphinx_proof/domain.py +++ b/sphinx_proof/domain.py @@ -161,7 +161,8 @@ def resolve_xref( number = ".".join( map(str, env.toc_fignumbers[todocname][countertyp][target]) ) - title = nodes.Text(f"{translate(match["realtype"].title())} {number}") + type_title = translate(match["realtype"].title()) + title = nodes.Text(f"{type_title} {number}") # builder, fromdocname, todocname, targetid, child, title=None return make_refnode(builder, fromdocname, todocname, target, title) else: From c34886502a007e028b44b4830b2dc921b8117fce Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 22:38:51 +0100 Subject: [PATCH 03/10] Add config validation and refactor proof type mapping Introduces a check_config_values function to validate Sphinx configuration values at runtime, ensuring correct types and defaults for proof-related settings. Also refactors DEFAULT_REALTYP_TO_COUNTERTYP in directive.py to dynamically use PROOF_TYPES, improving maintainability and consistency. --- sphinx_proof/__init__.py | 62 +++++++++++++++++++++++++++++++++++++++ sphinx_proof/directive.py | 22 +++----------- 2 files changed, 66 insertions(+), 18 deletions(-) diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index 7eb002a..5f037c0 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -108,6 +108,7 @@ def setup(app: Sphinx) -> Dict[str, Any]: app.add_config_value("proof_title_weight", "", "html") app.add_css_file("proof.css") + app.connect("config-inited", check_config_values) app.connect("build-finished", copy_asset_files) app.connect("config-inited", init_numfig) app.connect("env-purge-doc", purge_proofs) @@ -143,3 +144,64 @@ def setup(app: Sphinx) -> Dict[str, Any]: "parallel_read_safe": True, "parallel_write_safe": True, } + + +def check_config_values(app: Sphinx, config: Config) -> None: + """Check configuration values.""" + # Check if proof_minimal_theme is boolean + if not isinstance(config.proof_minimal_theme, bool): + logger.warning( + "'proof_minimal_theme' config value must be a boolean. " + "Using default value False." + ) + config.proof_minimal_theme = False + + # Check of prf_realtyp_to_countertyp is a dictionary + if not isinstance(config.prf_realtyp_to_countertyp, dict): + logger.warning( + "'prf_realtyp_to_countertyp' config value must be a dictionary. " + "Using default empty dictionary." + ) + config.prf_realtyp_to_countertyp = {} + # Check if each key and each value in prf_realtyp_to_countertyp + # is a valid proof type + for key, value in config.prf_realtyp_to_countertyp.items(): + if key not in PROOF_TYPES: + logger.warning( + f"Key '{key}' in 'prf_realtyp_to_countertyp' is not " + "a valid proof type. " + "It will be removed." + ) + del config.prf_realtyp_to_countertyp[key] + elif value not in PROOF_TYPES: + logger.warning( + f"Value '{value}' in 'prf_realtyp_to_countertyp' is not " + "a valid proof type. It will be removed." + ) + del config.prf_realtyp_to_countertyp[key] + # Check if proof_title_format is a string + if not isinstance(config.proof_title_format, str): + logger.warning( + "'proof_title_format' config value must be a string." + "Using default value ' (%t)'." + ) + config.proof_title_format = " (%t)" + elif "%t" not in config.proof_title_format: + logger.warning( + "'proof_title_format' config value must contain the " + "substring '%t' to print a title." + ) + # Check if proof_number_weight is a string + if not isinstance(config.proof_number_weight, str): + logger.warning( + "'proof_number_weight' config value must be a string. " + "Using default value ''." + ) + config.proof_number_weight = "" + # Check if proof_title_weight is a string + if not isinstance(config.proof_title_weight, str): + logger.warning( + "'proof_title_weight' config value must be a string. " + "Using default value ''." + ) + config.proof_title_weight = "" diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 2f0b46a..40e2a39 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -16,27 +16,13 @@ from sphinx.util.docutils import SphinxDirective from .nodes import unenumerable_node, NODE_TYPES from .nodes import proof_node +from .proof_type import PROOF_TYPES 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", -} +DEFAULT_REALTYP_TO_COUNTERTYP = {} +for proof_type in PROOF_TYPES: + DEFAULT_REALTYP_TO_COUNTERTYP[proof_type] = proof_type class ElementDirective(SphinxDirective): From 593ad75eec84b9158870e657659772faed24ebe7 Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 22:42:52 +0100 Subject: [PATCH 04/10] Move DEFAULT_REALTYP_TO_COUNTERTYP to proof_type.py Refactored the definition of DEFAULT_REALTYP_TO_COUNTERTYP from directive.py to proof_type.py for better separation of concerns and to avoid circular imports. Updated imports accordingly. Minor changes to test files only add missing newlines at end of file. --- sphinx_proof/directive.py | 6 +----- sphinx_proof/proof_type.py | 4 ++++ .../algorithm/_algo_labeled_titled_with_classname.html | 2 +- tests/test_html/algorithm/_algo_nonumber.html | 2 +- tests/test_html/algorithm/_algo_numbered_reference.html | 2 +- tests/test_html/algorithm/_algo_text_reference.html | 2 +- tests/test_html/proof/_proof_no_classname.html | 2 +- tests/test_html/proof/_proof_with_argument_content.html | 2 +- tests/test_html/proof/_proof_with_classname.html | 2 +- tests/test_html/proof/_proof_with_unlabeled_math.html | 2 +- tests/test_latex/test_latex_build.tex | 2 +- 11 files changed, 14 insertions(+), 14 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 40e2a39..df07915 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -16,14 +16,10 @@ from sphinx.util.docutils import SphinxDirective from .nodes import unenumerable_node, NODE_TYPES from .nodes import proof_node -from .proof_type import PROOF_TYPES +from .proof_type import DEFAULT_REALTYP_TO_COUNTERTYP logger = logging.getLogger(__name__) -DEFAULT_REALTYP_TO_COUNTERTYP = {} -for proof_type in PROOF_TYPES: - DEFAULT_REALTYP_TO_COUNTERTYP[proof_type] = proof_type - class ElementDirective(SphinxDirective): """A custom Sphinx Directive""" diff --git a/sphinx_proof/proof_type.py b/sphinx_proof/proof_type.py index 5a079aa..f14675b 100644 --- a/sphinx_proof/proof_type.py +++ b/sphinx_proof/proof_type.py @@ -118,3 +118,7 @@ class NotationDirective(ElementDirective): "assumption": AssumptionDirective, "notation": NotationDirective, } + +DEFAULT_REALTYP_TO_COUNTERTYP = {} +for proof_type in PROOF_TYPES: + DEFAULT_REALTYP_TO_COUNTERTYP[proof_type] = proof_type diff --git a/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html b/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html index 98ee3e9..b90646d 100644 --- a/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html +++ b/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html @@ -3,4 +3,4 @@

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- + \ No newline at end of file diff --git a/tests/test_html/algorithm/_algo_nonumber.html b/tests/test_html/algorithm/_algo_nonumber.html index d65590b..a0b5696 100644 --- a/tests/test_html/algorithm/_algo_nonumber.html +++ b/tests/test_html/algorithm/_algo_nonumber.html @@ -3,4 +3,4 @@

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- + \ No newline at end of file diff --git a/tests/test_html/algorithm/_algo_numbered_reference.html b/tests/test_html/algorithm/_algo_numbered_reference.html index 97df9d8..d86c8a3 100644 --- a/tests/test_html/algorithm/_algo_numbered_reference.html +++ b/tests/test_html/algorithm/_algo_numbered_reference.html @@ -1 +1 @@ -

referencing with number Algorithm 1.

+

referencing with number Algorithm 1.

\ No newline at end of file diff --git a/tests/test_html/algorithm/_algo_text_reference.html b/tests/test_html/algorithm/_algo_text_reference.html index f30a697..2106765 100644 --- a/tests/test_html/algorithm/_algo_text_reference.html +++ b/tests/test_html/algorithm/_algo_text_reference.html @@ -1 +1 @@ -

referencing with text: text.

+

referencing with text: text.

\ No newline at end of file diff --git a/tests/test_html/proof/_proof_no_classname.html b/tests/test_html/proof/_proof_no_classname.html index d469b3d..3613cfe 100644 --- a/tests/test_html/proof/_proof_no_classname.html +++ b/tests/test_html/proof/_proof_no_classname.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur.

Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- + \ No newline at end of file diff --git a/tests/test_html/proof/_proof_with_argument_content.html b/tests/test_html/proof/_proof_with_argument_content.html index a285425..01d6a79 100644 --- a/tests/test_html/proof/_proof_with_argument_content.html +++ b/tests/test_html/proof/_proof_with_argument_content.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua.

Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- + \ No newline at end of file diff --git a/tests/test_html/proof/_proof_with_classname.html b/tests/test_html/proof/_proof_with_classname.html index d623c0e..f605a6e 100644 --- a/tests/test_html/proof/_proof_with_classname.html +++ b/tests/test_html/proof/_proof_with_classname.html @@ -1,3 +1,3 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

-
+ \ No newline at end of file diff --git a/tests/test_html/proof/_proof_with_unlabeled_math.html b/tests/test_html/proof/_proof_with_unlabeled_math.html index c0e93a0..e1ef2da 100644 --- a/tests/test_html/proof/_proof_with_unlabeled_math.html +++ b/tests/test_html/proof/_proof_with_unlabeled_math.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut

\[P_t(x, y) = \mathbb 1\{x = y\} + t Q(x, y) + o(t)\]
- + \ No newline at end of file diff --git a/tests/test_latex/test_latex_build.tex b/tests/test_latex/test_latex_build.tex index 19f308a..64153d2 100644 --- a/tests/test_latex/test_latex_build.tex +++ b/tests/test_latex/test_latex_build.tex @@ -146,4 +146,4 @@ \chapter{content 5} \renewcommand{\indexname}{Index} \printindex -\end{document} +\end{document} \ No newline at end of file From d6c4b31331fa22d8c372624107af4c1bbaf99ff1 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 24 Jan 2026 21:43:01 +0000 Subject: [PATCH 05/10] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- .../algorithm/_algo_labeled_titled_with_classname.html | 2 +- tests/test_html/algorithm/_algo_nonumber.html | 2 +- tests/test_html/algorithm/_algo_numbered_reference.html | 2 +- tests/test_html/algorithm/_algo_text_reference.html | 2 +- tests/test_html/proof/_proof_no_classname.html | 2 +- tests/test_html/proof/_proof_with_argument_content.html | 2 +- tests/test_html/proof/_proof_with_classname.html | 2 +- tests/test_html/proof/_proof_with_unlabeled_math.html | 2 +- tests/test_latex/test_latex_build.tex | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html b/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html index b90646d..98ee3e9 100644 --- a/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html +++ b/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html @@ -3,4 +3,4 @@

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/algorithm/_algo_nonumber.html b/tests/test_html/algorithm/_algo_nonumber.html index a0b5696..d65590b 100644 --- a/tests/test_html/algorithm/_algo_nonumber.html +++ b/tests/test_html/algorithm/_algo_nonumber.html @@ -3,4 +3,4 @@

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/algorithm/_algo_numbered_reference.html b/tests/test_html/algorithm/_algo_numbered_reference.html index d86c8a3..97df9d8 100644 --- a/tests/test_html/algorithm/_algo_numbered_reference.html +++ b/tests/test_html/algorithm/_algo_numbered_reference.html @@ -1 +1 @@ -

referencing with number Algorithm 1.

\ No newline at end of file +

referencing with number Algorithm 1.

diff --git a/tests/test_html/algorithm/_algo_text_reference.html b/tests/test_html/algorithm/_algo_text_reference.html index 2106765..f30a697 100644 --- a/tests/test_html/algorithm/_algo_text_reference.html +++ b/tests/test_html/algorithm/_algo_text_reference.html @@ -1 +1 @@ -

referencing with text: text.

\ No newline at end of file +

referencing with text: text.

diff --git a/tests/test_html/proof/_proof_no_classname.html b/tests/test_html/proof/_proof_no_classname.html index 3613cfe..d469b3d 100644 --- a/tests/test_html/proof/_proof_no_classname.html +++ b/tests/test_html/proof/_proof_no_classname.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur.

Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/proof/_proof_with_argument_content.html b/tests/test_html/proof/_proof_with_argument_content.html index 01d6a79..a285425 100644 --- a/tests/test_html/proof/_proof_with_argument_content.html +++ b/tests/test_html/proof/_proof_with_argument_content.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua.

Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/proof/_proof_with_classname.html b/tests/test_html/proof/_proof_with_classname.html index f605a6e..d623c0e 100644 --- a/tests/test_html/proof/_proof_with_classname.html +++ b/tests/test_html/proof/_proof_with_classname.html @@ -1,3 +1,3 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

-
\ No newline at end of file + diff --git a/tests/test_html/proof/_proof_with_unlabeled_math.html b/tests/test_html/proof/_proof_with_unlabeled_math.html index e1ef2da..c0e93a0 100644 --- a/tests/test_html/proof/_proof_with_unlabeled_math.html +++ b/tests/test_html/proof/_proof_with_unlabeled_math.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut

\[P_t(x, y) = \mathbb 1\{x = y\} + t Q(x, y) + o(t)\]
- \ No newline at end of file + diff --git a/tests/test_latex/test_latex_build.tex b/tests/test_latex/test_latex_build.tex index 64153d2..19f308a 100644 --- a/tests/test_latex/test_latex_build.tex +++ b/tests/test_latex/test_latex_build.tex @@ -146,4 +146,4 @@ \chapter{content 5} \renewcommand{\indexname}{Index} \printindex -\end{document} \ No newline at end of file +\end{document} From b6d6af374f8b6edc6e0975faefaafe755e7f41d1 Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 22:45:02 +0100 Subject: [PATCH 06/10] Inline DEFAULT_REALTYP_TO_COUNTERTYP mapping in directive.py Moved the DEFAULT_REALTYP_TO_COUNTERTYP dictionary from proof_type.py directly into directive.py to remove the import and simplify dependencies. Updated test HTML and LaTeX files to ensure proper newline at end of file. --- sphinx_proof/directive.py | 20 ++++++++++++++++++- .../_algo_labeled_titled_with_classname.html | 2 +- tests/test_html/algorithm/_algo_nonumber.html | 2 +- .../algorithm/_algo_numbered_reference.html | 2 +- .../algorithm/_algo_text_reference.html | 2 +- .../test_html/proof/_proof_no_classname.html | 2 +- .../proof/_proof_with_argument_content.html | 2 +- .../proof/_proof_with_classname.html | 2 +- .../proof/_proof_with_unlabeled_math.html | 2 +- tests/test_latex/test_latex_build.tex | 2 +- 10 files changed, 28 insertions(+), 10 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index df07915..2f0b46a 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -16,11 +16,29 @@ from sphinx.util.docutils import SphinxDirective from .nodes import unenumerable_node, NODE_TYPES from .nodes import proof_node -from .proof_type import DEFAULT_REALTYP_TO_COUNTERTYP 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""" diff --git a/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html b/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html index b90646d..98ee3e9 100644 --- a/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html +++ b/tests/test_html/algorithm/_algo_labeled_titled_with_classname.html @@ -3,4 +3,4 @@

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/algorithm/_algo_nonumber.html b/tests/test_html/algorithm/_algo_nonumber.html index a0b5696..d65590b 100644 --- a/tests/test_html/algorithm/_algo_nonumber.html +++ b/tests/test_html/algorithm/_algo_nonumber.html @@ -3,4 +3,4 @@

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/algorithm/_algo_numbered_reference.html b/tests/test_html/algorithm/_algo_numbered_reference.html index d86c8a3..97df9d8 100644 --- a/tests/test_html/algorithm/_algo_numbered_reference.html +++ b/tests/test_html/algorithm/_algo_numbered_reference.html @@ -1 +1 @@ -

referencing with number Algorithm 1.

\ No newline at end of file +

referencing with number Algorithm 1.

diff --git a/tests/test_html/algorithm/_algo_text_reference.html b/tests/test_html/algorithm/_algo_text_reference.html index 2106765..f30a697 100644 --- a/tests/test_html/algorithm/_algo_text_reference.html +++ b/tests/test_html/algorithm/_algo_text_reference.html @@ -1 +1 @@ -

referencing with text: text.

\ No newline at end of file +

referencing with text: text.

diff --git a/tests/test_html/proof/_proof_no_classname.html b/tests/test_html/proof/_proof_no_classname.html index 3613cfe..d469b3d 100644 --- a/tests/test_html/proof/_proof_no_classname.html +++ b/tests/test_html/proof/_proof_no_classname.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur.

Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/proof/_proof_with_argument_content.html b/tests/test_html/proof/_proof_with_argument_content.html index 01d6a79..a285425 100644 --- a/tests/test_html/proof/_proof_with_argument_content.html +++ b/tests/test_html/proof/_proof_with_argument_content.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua.

Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

- \ No newline at end of file + diff --git a/tests/test_html/proof/_proof_with_classname.html b/tests/test_html/proof/_proof_with_classname.html index f605a6e..d623c0e 100644 --- a/tests/test_html/proof/_proof_with_classname.html +++ b/tests/test_html/proof/_proof_with_classname.html @@ -1,3 +1,3 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

-
\ No newline at end of file + diff --git a/tests/test_html/proof/_proof_with_unlabeled_math.html b/tests/test_html/proof/_proof_with_unlabeled_math.html index e1ef2da..c0e93a0 100644 --- a/tests/test_html/proof/_proof_with_unlabeled_math.html +++ b/tests/test_html/proof/_proof_with_unlabeled_math.html @@ -2,4 +2,4 @@

Proof. Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut

\[P_t(x, y) = \mathbb 1\{x = y\} + t Q(x, y) + o(t)\]
- \ No newline at end of file + diff --git a/tests/test_latex/test_latex_build.tex b/tests/test_latex/test_latex_build.tex index 64153d2..19f308a 100644 --- a/tests/test_latex/test_latex_build.tex +++ b/tests/test_latex/test_latex_build.tex @@ -146,4 +146,4 @@ \chapter{content 5} \renewcommand{\indexname}{Index} \printindex -\end{document} \ No newline at end of file +\end{document} From a33704a884bfdc679bb65349587d656632692251 Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 22:49:54 +0100 Subject: [PATCH 07/10] Move DEFAULT_REALTYP_TO_COUNTERTYP to proof_type.py Relocated the DEFAULT_REALTYP_TO_COUNTERTYP mapping from directive.py to proof_type.py for better modularity and to centralize proof type definitions. --- sphinx_proof/directive.py | 20 +------------------- sphinx_proof/proof_type.py | 20 +++++++++++++++++--- 2 files changed, 18 insertions(+), 22 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 2f0b46a..df07915 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -16,29 +16,11 @@ from sphinx.util.docutils import SphinxDirective from .nodes import unenumerable_node, NODE_TYPES from .nodes import proof_node +from .proof_type import DEFAULT_REALTYP_TO_COUNTERTYP 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""" diff --git a/sphinx_proof/proof_type.py b/sphinx_proof/proof_type.py index f14675b..99070c5 100644 --- a/sphinx_proof/proof_type.py +++ b/sphinx_proof/proof_type.py @@ -119,6 +119,20 @@ class NotationDirective(ElementDirective): "notation": NotationDirective, } -DEFAULT_REALTYP_TO_COUNTERTYP = {} -for proof_type in PROOF_TYPES: - DEFAULT_REALTYP_TO_COUNTERTYP[proof_type] = proof_type +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", +} From 72293a50db6a61780e3401f073f44f1ad7065724 Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 23:42:15 +0100 Subject: [PATCH 08/10] Move DEFAULT_REALTYP_TO_COUNTERTYP to directive.py Relocated the DEFAULT_REALTYP_TO_COUNTERTYP dictionary from proof_type.py to directive.py to improve module organization and reduce unnecessary imports. --- sphinx_proof/directive.py | 20 +++++++++++++++++++- sphinx_proof/proof_type.py | 18 ------------------ 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index df07915..2f0b46a 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -16,11 +16,29 @@ from sphinx.util.docutils import SphinxDirective from .nodes import unenumerable_node, NODE_TYPES from .nodes import proof_node -from .proof_type import DEFAULT_REALTYP_TO_COUNTERTYP 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""" diff --git a/sphinx_proof/proof_type.py b/sphinx_proof/proof_type.py index 99070c5..5a079aa 100644 --- a/sphinx_proof/proof_type.py +++ b/sphinx_proof/proof_type.py @@ -118,21 +118,3 @@ class NotationDirective(ElementDirective): "assumption": AssumptionDirective, "notation": NotationDirective, } - -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", -} From 9e3391bd6d372f828ae3a82c8799f92465ac22d1 Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 23:44:09 +0100 Subject: [PATCH 09/10] Refactor proof type mapping to use PROOF_TYPES Replaces the hardcoded DEFAULT_REALTYP_TO_COUNTERTYP dictionary with a dynamic construction based on PROOF_TYPES from proof_type.py. This improves maintainability by centralizing proof type definitions. --- sphinx_proof/directive.py | 22 ++++------------------ 1 file changed, 4 insertions(+), 18 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 2f0b46a..711edc0 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -16,27 +16,13 @@ from sphinx.util.docutils import SphinxDirective from .nodes import unenumerable_node, NODE_TYPES from .nodes import proof_node +from .proof_type import PROOF_TYPES 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", -} +DEFAULT_REALTYP_TO_COUNTERTYP = {} +for typ in PROOF_TYPES: + DEFAULT_REALTYP_TO_COUNTERTYP[typ] = typ class ElementDirective(SphinxDirective): From f51aa519c0ccb1297fb3832c3f5d5457ded9f5cc Mon Sep 17 00:00:00 2001 From: Dennis den Ouden-van der Horst Date: Sat, 24 Jan 2026 23:45:20 +0100 Subject: [PATCH 10/10] Inline DEFAULT_REALTYP_TO_COUNTERTYP mapping Replaces dynamic construction of DEFAULT_REALTYP_TO_COUNTERTYP from PROOF_TYPES with a static dictionary definition. This change removes the dependency on PROOF_TYPES and makes the mapping explicit within directive.py. --- sphinx_proof/directive.py | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py index 711edc0..2f0b46a 100644 --- a/sphinx_proof/directive.py +++ b/sphinx_proof/directive.py @@ -16,13 +16,27 @@ from sphinx.util.docutils import SphinxDirective from .nodes import unenumerable_node, NODE_TYPES from .nodes import proof_node -from .proof_type import PROOF_TYPES logger = logging.getLogger(__name__) -DEFAULT_REALTYP_TO_COUNTERTYP = {} -for typ in PROOF_TYPES: - DEFAULT_REALTYP_TO_COUNTERTYP[typ] = typ + +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):