Zulip Chat Archive

Stream: general

Topic: comments highlighting

Patrick Massot (Jul 09 2020 at 21:57):

In the VSCode extension, docstrings get some syntax highlighting, at least for stuff between backticks. Is there any obstacle to getting the same thing in comments?

Mario Carneiro (Jul 09 2020 at 23:11):

@Patrick Massot Is this maybe in the wrong stream?

Patrick Massot (Jul 09 2020 at 23:43):

Indeed. I wanted to put this in general. Could you move it?

Notification Bot (Jul 10 2020 at 00:05):

This topic was moved here from #Lean Together 2019 > comments highlighting by Mario Carneiro

Gabriel Ebner (Jul 10 2020 at 08:33):

The reason markdown highlighting was restricted to doc and module doc comments is because it has semantic meaning there (the documentation generation tool expects markdown there).

Patrick Massot (Jul 10 2020 at 08:43):

Thanks Gabriel, but it doesn't seem to work :sad:

Patrick Massot (Jul 10 2020 at 08:43):

I'm on 1.16.2 and still don't see my backticks

Gabriel Ebner (Jul 10 2020 at 08:50):

Maybe I misunderstood you. Backticks in comments are highlighted for me: backtick_highlighting.png

Patrick Massot (Jul 10 2020 at 08:52):

This is indeed what I asked for, but I don't get it here.

Gabriel Ebner (Jul 10 2020 at 08:54):

Have you restarted vscode after the extension update?

Patrick Massot (Jul 10 2020 at 08:54):

Oh I missed a "reload required" button!

Patrick Massot (Jul 10 2020 at 08:54):

I thought I restarted it.

Patrick Massot (Jul 10 2020 at 08:55):

Thanks a lot!

Last updated: Dec 20 2023 at 11:08 UTC