-
Notifications
You must be signed in to change notification settings - Fork 119
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
refactor: port mistletoe + MathJax changes from doc-gen #165
Conversation
```latex | ||
You can use LaTeX using `$$` to enclose inline LaTeX and | ||
````md | ||
```math |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This, at least, was wrong previously.
Is this consistent with |
It will be now that leanprover-community/doc-gen#110 is merged. (I will try to backport some of the MathJax related changes here next.) |
Actually, let me rework this more along the lines of leanprover-community/doc-gen#110. Namely, I want to see if I can factor out the markdown processing into another module like I did there. |
|
This ports the changes to the mistletoe CustomHTMLRenderer class from leanprover-community/doc-gen#110 that are needed to make it work well with MathJax:
CustomHTMLRenderer
code tomistletoe_renderer.py
mathjax_editing.py
(only called bymistletoe_renderer
)latex.md
(will be viewable at https://leanprover-community.github.io/latex.html after this is deployed, but should not be linked to from anywhere else)One non-MathJax-related change in behavior in
CustomHTMLRenderer
is that the syntax highlighting now defaults tolean
, rather than attempting to guess a language. This makes it agree with both Zulip anddoc-gen
. I thus added info strings to the markdown files that needed them.