Zulip Chat Archive

Stream: Codewars

Topic: syntax highlighter


view this post on Zulip Kenny Lau (May 19 2020 at 08:01):

What's the syntax highlighter used? It doesn't highlight theorem or lemma or by and it doesn't comment out comments /- I am a comment -/

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

view this post on Zulip Shing Tak Lam (May 19 2020 at 08:31):

Yeah it does seem to be the case. It highlights constructor and quote which aren't Lean keywords.

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