Zulip Chat Archive

Stream: general

Topic: Module.End breaks VS Code bracket colors


Kevin Buzzard (May 30 2022 at 14:54):

ModuleEnd.png

All my nicely-paired-up brackets are red! The code compiles fine. Experimentation indicates that the issue is some parser treating End as ...however end is treated (some sort of deliminator?). This is with VS Code's default bracket pair colorizer. Can I fix this somehow? (right now I'm using notation Mend for Module.End!)

Eric Wieser (May 30 2022 at 15:50):

begin/end are considered brackets by the vscode syntax

Eric Wieser (May 30 2022 at 15:51):

https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/language-configuration.json#L47

Kevin Buzzard (May 30 2022 at 17:34):

But is this not case sensitive?

Gabriel Ebner (May 30 2022 at 17:37):

See also https://github.com/leanprover/vscode-lean4/issues/174

Gabriel Ebner (May 30 2022 at 17:37):

There's a similar highlighting issue with

section
end

Gabriel Ebner (May 30 2022 at 17:38):

Maybe we should just remove begin/end from the list of brackets.

Gabriel Ebner (May 30 2022 at 17:38):

Oh, yet another issue: https://github.com/leanprover/vscode-lean/issues/282

Eric Wieser (May 30 2022 at 17:43):

Probably we should file an upstream issue here

Eric Wieser (May 30 2022 at 17:44):

Case insensitive, word-boundary-agnostic matches on bracket characters feels ridiculous

Patrick Massot (May 30 2022 at 18:08):

Yes, the highlighting bug for end at the end of a section is really annoying.

Gabriel Ebner (May 30 2022 at 18:54):

That one's "fixed" now, but we had to give up the bracket-matching in return.


Last updated: Dec 20 2023 at 11:08 UTC