Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for assumption directive #73 #80

Merged
merged 5 commits into from
Jul 14, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

This package contains a [Sphinx](http://www.sphinx-doc.org/en/master/) extension
for producing proof, theorem, axiom, lemma, definition, criterion, remark, conjecture,
corollary, algorithm, example, property, observation and proposition directives.
corollary, algorithm, example, property, observation, proposition and assumption directives.


## Get started
Expand Down
2 changes: 1 addition & 1 deletion docs/source/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ zreferences

This package contains a [Sphinx](http://www.sphinx-doc.org/en/master/) extension
for producing proof, theorem, axiom, lemma, definition, criterion, remark, conjecture,
corollary, algorithm, example, property, observation and proposition directives.
corollary, algorithm, example, property, observation, proposition and assumption directives.

**Features**:

Expand Down
37 changes: 37 additions & 0 deletions docs/source/syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -696,6 +696,43 @@ This is a dummy proposition directive.

You can refer to a proposition using the `{prf:ref}` role like: ```{prf:ref}`my-proposition` ```, which will replace the reference with the proposition number like so: {prf:ref}`my-proposition`. When an explicit text is provided, this caption will serve as the title of the reference.


### Assumptions

An assumption directive can be included using the `prf:assumption` pattern. The directive is enumerated by default and can take in an optional title argument. The following options are also supported:

* `label` : text

A unique identifier for your assumption that you can use to reference it with `{prf:ref}`. Cannot contain spaces or special characters.
* `class` : text

Value of the assumption’s class attribute which can be used to add custom CSS or JavaScript.
* `nonumber` : flag (empty)

Turns off assumption auto numbering.

**Example**

```{prf:assumption}
:label: my-assumption
This is a dummy assumption directive.
```

**MyST Syntax**

``````md
```{prf:assumption}
:label: my-assumption

This is a dummy assumption directive.
```
``````

#### Referencing Assumptions

You can refer to an assumption using the `{prf:ref}` role like: ```{prf:ref}`my-assumption` ```, which will replace the reference with the assumption number like so: {prf:ref}`my-assumption`. When an explicit text is provided, this caption will serve as the title of the reference.

## How to Hide Content

Directive content can be hidden using the `dropdown` class which is available through [sphinx-togglebutton](https://sphinx-togglebutton.readthedocs.io/en/latest/). If your project utilizes the [MyST-NB](https://myst-nb.readthedocs.io/en/latest/) extension, there is no need to activate `sphinx-togglebutton` since it is already bundled with `MyST-NB`.
Expand Down
3 changes: 2 additions & 1 deletion setup.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@
LONG_DESCRIPTION = """
This package contains a [Sphinx](http://www.sphinx-doc.org/en/master/) extension
for producing proof, theorem, axiom, lemma, definition, criterion, remark, conjecture,
corollary, algorithm, example, property, observation and proposition directives.
corollary, algorithm, example, property, observation, proposition, and
assumption directives.
This project is maintained and supported by [najuzilu](https://github.com/najuzilu).
"""
Expand Down
11 changes: 11 additions & 0 deletions sphinx_proof/_static/proof.css
Original file line number Diff line number Diff line change
Expand Up @@ -194,3 +194,14 @@ div.proposition {
div.proposition p.admonition-title {
background-color: var(--note-title-color);
}
/*********************************************
* Assumption *
*********************************************/
div.assumption {
border-color: var(--hint-border-color);
background-color: var(--hint-title-color);
}

div.assumption p.admonition-title {
background-color: var(--hint-title-color);
}
5 changes: 5 additions & 0 deletions sphinx_proof/nodes.py
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,10 @@ class unenumerable_node(nodes.Admonition, nodes.Element):
pass


class assumption_node(nodes.Admonition, nodes.Element):
pass


NODE_TYPES = {
"axiom": axiom_node,
"theorem": theorem_node,
Expand All @@ -197,4 +201,5 @@ class unenumerable_node(nodes.Admonition, nodes.Element):
"property": property_node,
"observation": observation_node,
"proposition": proposition_node,
"assumption": assumption_node,
}
7 changes: 7 additions & 0 deletions sphinx_proof/proof_type.py
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,12 @@ class PropositionDirective(ElementDirective):
name = "proposition"


class AssumptionDirective(ElementDirective):
"""A custom assumption directive."""

name = "assumption"


PROOF_TYPES = {
"axiom": AxiomDirective,
"theorem": TheoremDirective,
Expand All @@ -103,4 +109,5 @@ class PropositionDirective(ElementDirective):
"property": PropertyDirective,
"observation": ObservationDirective,
"proposition": PropositionDirective,
"assumption": AssumptionDirective,
}
1 change: 1 addition & 0 deletions sphinx_proof/translations/jsons/Assumption.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
[{"language":"English","symbol":"en","text":"Assumption"}]