## 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.

green_and_red.png

#### 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: May 18 2021 at 17:44 UTC