Custom highlighting

Stream: general

[Bhavik Mehta]

I'd like to play with what's highlighted in vscode - is there a way I can easily customize which tokens/keywords are highlighted and how?

[Jasmin Blanchette]

You need to talk to @Gabriel Ebner for that. I believe the answer is no (depending of course on your definition of "easily").

[Mario Carneiro]

You can modify https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json to add your own keywords

[Mario Carneiro]

I think you can do this to your own local copy of vscode-lean (in ~/.vscode/extensions/jroesch.lean-x.y/) without a rebuild (only restarting the window)

[Gabriel Ebner]

The official way to work on the extension is described in the README: https://github.com/leanprover/vscode-lean#development

[Bhavik Mehta]

Cool thanks all!