Skip to content

Commit

Permalink
Support for assumption directive #73 (#80)
Browse files Browse the repository at this point in the history
* Support for assumption directive   #73

* pre-commit runs

* translation json for assumption directive

Co-authored-by: AakashGC <aakashguptachoudhury@gmail.com>
  • Loading branch information
shailesh1729 and AakashGfude committed Jul 14, 2022
1 parent 16ae061 commit d37495f
Show file tree
Hide file tree
Showing 8 changed files with 65 additions and 3 deletions.
2 changes: 1 addition & 1 deletion README.md
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
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
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
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
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
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
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
@@ -0,0 +1 @@
[{"language":"English","symbol":"en","text":"Assumption"}]

0 comments on commit d37495f

Please sign in to comment.