Ryan Lahfa (May 11 2020 at 23:17):
Hello, I'm writing some Beamer presentation using pandoc and wondered if there was any KDE syntax highlighting file (https://github.com/KDE/syntax-highlighting/tree/master/data/syntax) for Lean, apparently, not ; but I'm pretty sure that Pygments support Lean as a target, because
minted support Lean.
Does anyone how hard would it be to write one for Lean?
Bhavik Mehta (May 11 2020 at 23:18):
You could probably adapt one from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json and/or https://github.com/leanprover/lean/blob/master/extras/latex/lstlean.tex
Ryan Lahfa (May 11 2020 at 23:22):
Makes sense, I think the JSON looks easier to port, but it would require my full concentration to do this kind of stuff w/o errors
Bryan Gin-ge Chen (May 11 2020 at 23:26):
The master branch of pygments has a decent lexer for Lean. I'm hoping they'll cut a release soon so that we can get Zulip's syntax highlighting fixed and also start adding syntax highlighting to the docs and website.
Last updated: May 09 2021 at 19:11 UTC