Zulip Chat Archive

Stream: general

Topic: VS Code colour overload

Kevin Buzzard (Jul 10 2020 at 19:16):

Working on the real number game today. Got a bit of a shock with the below level. Compiles fine, but why is everything red? This is valid syntax for Mohammad Pedramfar's Lean game maker; the stuff in $ signs will be rendered as LaTeX.


Gabriel Ebner (Jul 10 2020 at 19:53):

It's not valid markdown though. Just put backticks around it like you would in doc strings. Since today, all comments have markdown highlighting, just like doc strings.

Gabriel Ebner (Jul 10 2020 at 19:55):

It is hard to make the highlighting work correctly even when there is invalid markdown. I could hack something in so that unclosed elements (<c) don't run forever. But I think it's the easiest solution to just turn it into valid markdown.

Last updated: Dec 20 2023 at 11:08 UTC