VS Code colour overload

Stream: general

[Kevin Buzzard]

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]

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]

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.