VScode color formatting messed up by ]"]

Stream: general

[Yaël Dillies]

Line 120 of group_theory/subgroup.leanis @[to_additive "See Note [custom simps projection]"] and the parser doesn't like that. It picks up the inner ] as closing the outer [ and then proceeds to color everything red until line 262, which is funnily enough another tag with weird mixup of quotes and square brackets: @[to_additive "Sum of a list of elements in an add_subgroup is in the add_subgroup."].
Anyway we can solve this (minor) issue?

[Yaël Dillies]

Ugh, even Zulip pukes on this one.

[Eric Wieser]

Here's the vscode syntax definition: https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json

[Eric Wieser]

I've written this style of syntax highlighter before (for other tmLanguage derivatives), so should be able to take a look; can anyone recommend a workflow for iterating on it in vscode?

[Yaël Dillies]

Oh thanks! because my biggest experience with regexp is parsing the list of Caius rooms to prepare for the ballot.

[Yaël Dillies]

I suspect it's the match on l.22 that should be made less greedy: { "match": "@\\[[^\\]]*\\]", "name": "storage.modifier.lean" },

[Eric Wieser]

It ought to be recursing into the grammar I think

[Eric Wieser]

This also fails: /-"test" -/

[Yaël Dillies]

Yeah, and isn't it already, at least partially?

[Eric Wieser]

@Gabriel Ebner, what is comment.block.string.lean for? You added it in https://github.com/leanprover/vscode-lean/commit/48ad01824958992fdc05f039435480a0e111cb4e

[Yaël Dillies]

I think it should be recursive, but apply the outermost color format.

[Eric Wieser]

Huh, didn't know this existed: https://github.com/leanprover-community/lean/pull/352

[Gabriel Ebner]

This is an alternative way to write string literals:

#eval /-"
Hello, world!
"-/

[Yaël Dillies]

Does that also mean it's a choice that some keywords are put in blue and other aren't?

[Yaël Dillies]

Tactic names, to be more precise.

[Eric Wieser]

Ok, I have a fix

[Eric Wieser]

https://github.com/leanprover/vscode-lean/pull/265

[Yaël Dillies]

I love it how you can just report something on Zulip and someone will fix it in the minute.

[Eric Rodriguez]

I was actually looking at this yesterday and thought that the only way was "manually" creating a couple of extra levels (as properly nested brackets isn't a regular language). Does VSCode let you have more flexibility in this?

[Eric Wieser]

Have a look at the PR

[Eric Wieser]

the tmLanguage highlighting system allows {"#include": "a previous bit of grammar"}

[Eric Wieser]

So in this case, I just told it to parse expressions within the []

[Eric Wieser]

If it's in the middle of parsing a string it won't parse the closing ], which is what we want

[Eric Wieser]

I made a small follow-up PR at https://github.com/leanprover/vscode-lean/pull/266, since I didn't quite finish the job the first time, and vscode crashed before I could beat @Gabriel Ebner to the merge!

[Bolton Bailey]

Here is an issue I noticed that might be related, and can potentially be closed now https://github.com/leanprover/vscode-lean/issues/260

[Eric Wieser]

Would you mind trying to reproduce it and producing a #mwe?

[Eric Rodriguez]

if I type exactly what's on the video, `nat isn't that colour anymore regardless:

import tactic

open expr

meta def is_constant_of (l : list name) : expr → bool
| (const a a_1) := a ∈ l
| _  := ff

#eval is_constant_of [`nat, `int] ℕ

[Eric Wieser]

Does the syntax highlighter know about `name s at all?

[Floris van Doorn]

Did these PRs also fix the tiny highlighting issue of

@[derive [has_reflect, inhabited]]

where the last ] is not highlighted?

[Eric Wieser]

Yes

[Eric Wieser]

I've pushed a fix for this bug to pygments too, meaning it will eventually end up back on zulip: https://github.com/pygments/pygments/pull/1817