Skip to content

Commit a2869c7

Browse files
committed
added numbering support for other directives
1 parent 60cd7f6 commit a2869c7

File tree

5 files changed

+65
-27
lines changed

5 files changed

+65
-27
lines changed

sphinx_proof/__init__.py

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,16 @@
1010
from sphinx.config import Config
1111
from sphinx.application import Sphinx
1212
from sphinx.environment import BuildEnvironment
13-
from .nodes import enumerable_node, visit_enumerable_node, depart_enumerable_node
14-
from .nodes import unenumerable_node, visit_unenumerable_node, depart_unenumerable_node
13+
from .nodes import visit_enumerable_node, depart_enumerable_node
14+
from .nodes import (
15+
NODE_TYPES,
16+
unenumerable_node,
17+
visit_unenumerable_node,
18+
depart_unenumerable_node,
19+
)
1520
from .nodes import proof_node, visit_proof_node, depart_proof_node
1621
from .domain import ProofDomain
22+
from .proof_type import PROOF_TYPES
1723
from sphinx.util import logging
1824
from sphinx.util.fileutil import copy_asset
1925

@@ -83,14 +89,15 @@ def setup(app: Sphinx) -> Dict[str, Any]:
8389
html=(visit_unenumerable_node, depart_unenumerable_node),
8490
latex=(visit_unenumerable_node, depart_unenumerable_node),
8591
)
86-
app.add_enumerable_node(
87-
enumerable_node,
88-
"proof",
89-
None,
90-
singlehtml=(visit_enumerable_node, depart_enumerable_node),
91-
html=(visit_enumerable_node, depart_enumerable_node),
92-
latex=(visit_enumerable_node, depart_enumerable_node),
93-
)
92+
for node in PROOF_TYPES.keys():
93+
app.add_enumerable_node(
94+
NODE_TYPES[node],
95+
node,
96+
None,
97+
singlehtml=(visit_enumerable_node, depart_enumerable_node),
98+
html=(visit_enumerable_node, depart_enumerable_node),
99+
latex=(visit_enumerable_node, depart_enumerable_node),
100+
)
94101

95102
return {
96103
"version": "builtin",

sphinx_proof/directive.py

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
from sphinx.util import logging
1414
from docutils.parsers.rst import directives
1515
from sphinx.util.docutils import SphinxDirective
16-
from .nodes import enumerable_node, unenumerable_node
16+
from .nodes import unenumerable_node, NODE_TYPES
1717
from .nodes import proof_node
1818

1919
logger = logging.getLogger(__name__)
@@ -37,7 +37,6 @@ def run(self) -> List[Node]:
3737
env = self.env
3838
typ = self.name.split(":")[1]
3939
serial_no = env.new_serialno()
40-
4140
if not hasattr(env, "proof_list"):
4241
env.proof_list = {}
4342

@@ -76,7 +75,8 @@ def run(self) -> List[Node]:
7675
if "nonumber" in self.options:
7776
node = unenumerable_node()
7877
else:
79-
node = enumerable_node()
78+
node_type = NODE_TYPES[typ]
79+
node = node_type()
8080

8181
node.document = self.state.document
8282
node += nodes.title(title_text, "", *textnodes)

sphinx_proof/domain.py

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -119,6 +119,9 @@ def resolve_xref(
119119

120120
todocname = match["docname"]
121121
title = contnode[0]
122+
import pdb
123+
124+
pdb.set_trace()
122125
if target in contnode[0]:
123126
number = ""
124127
if not env.proof_list[target]["nonumber"]:

sphinx_proof/nodes.py

Lines changed: 31 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,22 @@ class proof_node(nodes.Admonition, nodes.Element):
2020
pass
2121

2222

23+
class axiom_node(nodes.Admonition, nodes.Element):
24+
pass
25+
26+
27+
class theorem_node(nodes.Admonition, nodes.Element):
28+
pass
29+
30+
31+
class lemma_node(nodes.Admonition, nodes.Element):
32+
pass
33+
34+
35+
class algorithm_node(nodes.Admonition, nodes.Element):
36+
pass
37+
38+
2339
class enumerable_node(nodes.Admonition, nodes.Element):
2440
pass
2541

@@ -28,6 +44,14 @@ class unenumerable_node(nodes.Admonition, nodes.Element):
2844
pass
2945

3046

47+
NODE_TYPES = {
48+
"axiom": axiom_node,
49+
"theorem": theorem_node,
50+
"lemma": lemma_node,
51+
"algorithm": algorithm_node,
52+
}
53+
54+
3155
def visit_enumerable_node(self, node: Node) -> None:
3256
if isinstance(self, LaTeXTranslator):
3357
docname = find_parent(self.builder.env, node, "section")
@@ -40,13 +64,16 @@ def visit_enumerable_node(self, node: Node) -> None:
4064
def depart_enumerable_node(self, node: Node) -> None:
4165
typ = node.attributes.get("type", "")
4266
if isinstance(self, LaTeXTranslator):
43-
number = get_node_number(self, node)
67+
number = get_node_number(self, node, typ)
4468
idx = list_rindex(self.body, latex_admonition_start) + 2
4569
self.body.insert(idx, f"{typ.title()} {number}")
4670
self.body.append(latex_admonition_end)
4771
else:
4872
# Find index in list of 'Proof #'
49-
number = get_node_number(self, node)
73+
number = get_node_number(self, node, typ)
74+
import pdb
75+
76+
pdb.set_trace()
5077
idx = self.body.index(f"Proof {number} ")
5178
self.body[idx] = f"{typ.title()} {number} "
5279
self.body.append("</div>")
@@ -86,9 +113,8 @@ def depart_proof_node(self, node: Node) -> None:
86113
pass
87114

88115

89-
def get_node_number(self, node: Node) -> str:
116+
def get_node_number(self, node: Node, typ) -> str:
90117
"""Get the number for the directive node for HTML."""
91-
key = "proof"
92118
ids = node.attributes.get("ids", [])[0]
93119
if isinstance(self, LaTeXTranslator):
94120
docname = find_parent(self.builder.env, node, "section")
@@ -97,7 +123,7 @@ def get_node_number(self, node: Node) -> str:
97123
) # Latex does not have builder.fignumbers
98124
else:
99125
fignumbers = self.builder.fignumbers
100-
number = fignumbers.get(key, {}).get(ids, ())
126+
number = fignumbers.get(typ, {}).get(ids, ())
101127
return ".".join(map(str, number))
102128

103129

sphinx_proof/proof_type.py

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -93,14 +93,16 @@ class PropositionDirective(ElementDirective):
9393
"axiom": AxiomDirective,
9494
"theorem": TheoremDirective,
9595
"lemma": LemmaDirective,
96-
"definition": DefinitionDirective,
97-
"remark": RemarkDirective,
98-
"conjecture": ConjectureDirective,
99-
"corollary": CorollaryDirective,
10096
"algorithm": AlgorithmDirective,
101-
"criterion": CriterionDirective,
102-
"example": ExampleDirective,
103-
"property": PropertyDirective,
104-
"observation": ObservationDirective,
105-
"proposition": PropositionDirective,
10697
}
98+
99+
# "definition": DefinitionDirective,
100+
# "remark": RemarkDirective,
101+
# "conjecture": ConjectureDirective,
102+
# "corollary": CorollaryDirective,
103+
# "algorithm": AlgorithmDirective,
104+
# "criterion": CriterionDirective,
105+
# "example": ExampleDirective,
106+
# "property": PropertyDirective,
107+
# "observation": ObservationDirective,
108+
# "proposition": PropositionDirective,

0 commit comments

Comments
 (0)