VSCode brackets

Stream: lean4

[Thomas Murrills]

While looking at the extension's language-configuration.json for vscode-lean4#328, I noticed that some of Lean's modified brackets, like @[], were missing from the list. I made a draft PR to the extension to address this (and adjacent things): vscode-lean4#330.

If this tweak looks like a good idea, I'm happy to make it a real PR. :)

[Mario Carneiro]

I don't think @[] is a modified bracket

[Mario Carneiro]

it's just @ followed by [] brackets

[Thomas Murrills]

What does @ mean by itself, though?

[Thomas Murrills]

I mean, what aspect of its standalone meaning is relevant to its use in attribute brackets?

[Thomas Murrills]

(Unless maybe you mean that it's important to show that the fundamental thing is [] because that's how it's written with attribute [...], and @ ought to be thought of as a modifier to that whole thing rather than as a component in a composite left bracket...)

[Mario Carneiro]

yes, that

[Mario Carneiro]

in fact lean core generally refers to attributes using only brackets as in [inline] in comments and error messages, although I prefer to use @[inline] style to make it clear that it's an attribute as opposed to something else

[Thomas Murrills]

Hmm, I guess the other side of that is that if @[] is what's useful in conveying attributehood in practice, then maybe people really are inclined to think of @[] as its "own sort of brackets" anyway rather than as a @ in front of [], and maybe it's not so important to color them differently.

The benefit of viewing @[] as a single composite bracket is that—to me at least—adding an attribute becomes less visually busy and stands out just a little more since the @[] is colored uniformly. That's ultimately a matter of taste, but here's an example of what I mean:
Before; After

I don't feel strongly about this, but just wanted to offer that perspective. :)

[James Gallicchio]

vastly prefer the uniform coloring there fwiw. to me, @[] is all one syntax construct in the same way attribute [] is all one syntax construct. you can't not use square brackets in either case, so in both cases it's "part of the syntax"

[Eric Wieser]

Are you advocating that attribute [ should be a matching pair too?

[James Gallicchio]

I think it makes sense for the [ color in attribute [] to be the same command blue as the attribute, yeah. But unfortunately then everything is blue :joy: maybe we can change the color of attributes to something other than blue.

[Eric Wieser]

Note that the colors look quite different if you turn off bracket matching

[Thomas Murrills]

Hmm, I’m not sure if I’d personally go so far as to make attribute the same color as []! The space kills it for me; I feel like the syntax does (should) look like a normal command (e.g. def) followed by special brackets to isolate the attribute. For me, it’s that when using @[], the whole thing does sort of feel like it constitutes “special brackets” to some degree (see above for caveats), and more importantly, looks clearer visually (which I feel would not necessarily be the case with recoloring attribute). But again this is really just a matter of preference. Maybe we ought to have a poll. :)