Zulip Chat Archive

Stream: general

Topic: KDE syntax highlighting definition for Lean?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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