Zulip Chat Archive
Stream: general
Topic: Module.End breaks VS Code bracket colors
Kevin Buzzard (May 30 2022 at 14:54):
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):
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