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 f2a2e36..d2c6942 100644 --- a/docs/source/options.md +++ b/docs/source/options.md @@ -31,6 +31,61 @@ sphinx: 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). +```` + ## Title format By default, the directive titles are formatted as `Name x.y.z (Title)`, where `Name` is the name of the directive (e.g., Proof, Theorem, Definition), `x.y.z` is the numbering of the directive, and `Title` is the optional title provided by the user. diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py index 650caee..5f037c0 100644 --- a/sphinx_proof/__init__.py +++ b/sphinx_proof/__init__.py @@ -102,11 +102,13 @@ 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_config_value("proof_title_format", " (%t)", "html") - app.add_config_value("proof_number_weight", "", "env") - app.add_config_value("proof_title_weight", "", "env") + app.add_config_value("proof_number_weight", "", "html") + 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) @@ -142,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 43209e8..2f0b46a 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 = "" @@ -72,13 +94,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 @@ -90,17 +112,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] @@ -117,16 +140,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..7558a0f 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,12 @@ 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}") + 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: 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))