@ only treated as binary_operator_definitions in tlaplus-grammar.json

[lemmy]

@ is not a binary operator in EXCEPT expressions (regex doesn't match causing @ to be ignored in EXCEPT):

v' = [v EXCEPT ![i] = IF j>i THEN "black" ELSE @]

https://github.com/alygin/vscode-tlaplus/blob/cdb96e0446d8c1314ff318406bfc31fdb93f0495/languages/tlaplus-grammar.json#L173

[alygin]

You're right, there's no special rule in the grammar description to capture @s within EXCEPT expressions. But this is a TextMate grammar, it's not intendend to be full and absolutely accurate. One can easily find many edge cases where it doesn't work ideally.

This grammar's aim is to provide good enough syntax highlighting, which, I believe, it does.

But it surely can be improved. We can have a grammar rule that captures @s (and !s for that matter) inside EXCEPT exressions and assign some scope to them (variable.name for instance), which will make them highlighted. That should be pretty easy.

[lemmy]

Context is https://github.com/lemmy/vscode-tlaplus/commit/542ec937d77a6b892cf5739baac4c27522f8973f , which doesn't work for @ in Except because the grammar doesn't recognize it properly.

[alygin]

Hm, I'm not sure VSCode uses grammar to detect word boundaries, but I've drafted the missing grammar rule, you can check if it helps: https://github.com/alygin/vscode-tlaplus/commit/10ed763ca87b3e4b54aeac5b90f1208953ca3050

[lemmy]

https://github.com/microsoft/vscode/blob/main/src/vs/editor/common/model/wordHelper.ts#L8 is probably what causes document.getWordRangeAtPosition(position) to return undefined for a position that points at an @ (and strips off the prime from a primed variable).

[alygin]

Yes, but it's possible to define a custom word pattern for a language: wordPattern.

[alygin]

Starting from v1.5.4, both @s and !s are highligted in one-line EXCEPT expressions.