Topic: syntax highlighter
Kenny Lau (May 19 2020 at 08:01):
What's the syntax highlighter used? It doesn't highlight
by and it doesn't comment out comments
/- I am a comment -/
Shing Tak Lam (May 19 2020 at 08:30):
I did some digging into their JS, and I found this line in the file which I think is responsible for syntax highlighting/entry mode
case "lean": return "agda";
So I think Lean's using the Agda highlighter right now...
Shing Tak Lam (May 19 2020 at 08:31):
Yeah it does seem to be the case. It highlights
quote which aren't Lean keywords.
Bryan Gin-ge Chen (May 20 2020 at 01:28):
I happen to have a Lean mode for CodeMirror in this Observable notebook. I'll try to split it out into its own repo by the weekend.
Last updated: May 08 2021 at 22:13 UTC