leanprover/vscode-lean#268

Stream: PR reviews

[Eric Wieser]

I had a go at improving the syntax highlighting in leanprover/vscode-lean#268: the result is that binders are now highlighted:
image.png

I had a go at highlighting types too, but while it works that seems kind of noisy in a language dominated by types (unless you really like green):

image.png

Thoughts?

[Eric Wieser]

Thumbs up this comment if you want all types highlighted as entity.type.name (teal by default as in the screenshot), thumbs down if you don't

[Gabriel Ebner]

I trusted your PR blindly--do we now have the teal types or not?

[Eric Wieser]

No, we do not have the teal types in that PR

[Eric Wieser]

Unless you edit your color theme and manually set meta.type.lean (which is unstyled by default) to teal

[Eric Wieser]

Thanks for the release!