Add Theorems #107
Add Theorems #107
Conversation
| {lemma, title="Euclid"} | ||
| > If `$ p` is prime and divides `$ ab` then it divides `$ a` or `$ b`. | ||
|
|
||
| {corollary, title="Prime factorization"} | ||
| > Each number has a canonical decomposition into prime factors. | ||
|
|
||
| {theorem, title="The main theorem"} |
There was a problem hiding this comment.
Is there a reason you chose title over caption? I think using caption instead of title might be more consistent with all other configs.
There was a problem hiding this comment.
It is not a caption in the sense of a \\caption{} element in Latex. It's more closely a heading. It still might be the best fit for consistency.
| _cfg: &'a Config, proof: WithRange<Proof<'a>>, | ||
| gen: &mut Generator<'a, impl Backend<'a>, impl Write>, | ||
| ) -> Result<Self> { | ||
| let WithRange(element, _range) = proof; |
There was a problem hiding this comment.
Could you destructure the Proof here such that it becomes a hard error if we add a new property to it? I did this everywhere else for that exact reason. That way the compiler tells us wherever we need to change something once an attribute is added to something.
| ProofKind::Definition => "amsthm-definition", | ||
| ProofKind::Lemma => "amsthm-lemma", | ||
| ProofKind::Proof => "proof", | ||
| ProofKind::Theorem=> "amsthm-theorem", |
There was a problem hiding this comment.
| ProofKind::Theorem=> "amsthm-theorem", | |
| ProofKind::Theorem => "amsthm-theorem", |
| let kind = if let Some(prefix) = prefix { | ||
| match prefix.as_ref().element().as_ref() { | ||
| "corollary" => ProofKind::Corollary, | ||
| "definition" => ProofKind::Definition, | ||
| "lemma" => ProofKind::Lemma, | ||
| "proof" => ProofKind::Proof, | ||
| "theorem" => ProofKind::Theorem, | ||
| other => { | ||
| self.diagnostics | ||
| .error(format!("unknown quote environment {:?}", other)) | ||
| .with_error_section(prefix.range(), "type defined here") | ||
| .emit(); | ||
| return; | ||
| } | ||
| } | ||
| } else { | ||
| self.diagnostics | ||
| .error("quote environment has no type") | ||
| .with_error_section(range, "configuration defined here") | ||
| .help("try indicating the type, the configuration could look like") | ||
| .help(" {proof}") | ||
| .emit(); | ||
| return; | ||
| }; |
There was a problem hiding this comment.
What if I want to have a quote within a figure with a caption, or a quote with a label? We don't support that right now, but with a change like this, I think we should support it in the long run. If you don't want to change it right now, could you please open an issue?
|
In general I'd still prefer using the already established code-blocks for this, but as you said, it doesn't have an existing infrastructure surrounding using markdown within the code-block. If we use code-blocks instead of quotes for this, we should be able to allow markdown-parsing by feeding the code-block-content back into pulldown-cmark. I think this might be the better solution syntax-wise, but might result in a harder infrastructure. |
|
I don't think it would be possible with a change short of forking pulldown_cmark. It would require a feedback mode where it is possible to insert content into the source code, potentially affecting even the tokenization stage within the parser. Not to mention all other kinds of events where the parser does look-ahead, for example for link callbacks. Also, the solution would only work in heradoc. It would not work in any other tool, which means no editor support, no refactoring support, etc. This compatibility was one primary motivation behind the other syntax choices—including includes and label/description that's proposed. I'm content with the Configuration extension for features that do not affect Markdown parsing but wouldn't use it beyond that. |
The end event is necessarily fits the beginning one as the causing front end event is the end of the corresponding Markdown code block. This makes redundant to check for this correspondence by splitting the tags. It also wrongly suggests duplicating the logic for handling the (latex formatted) math content.
They are specifically defined in such a way in the front end as to allow nesting of other Markdown elements inside their description. This makes it more natural to have theorems not only consisting of math blocks while allowing the natural nesting of them.
During some rework this did no longer have a context with an output stream available. This fixes it by writing directly to the underlying output stream.
Introduces support for theorems and proofs with very slight extensions to the syntax. Quotes are allowed to have configuration which previously was not possible. This makes them a useful element for embedding scoped content in which the Markdown semantics should be preserved.
Closes: #104