Zulip Chat Archive

Stream: general

Topic: Custom highlighting


Bhavik Mehta (Apr 21 2020 at 12:36):

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 (Apr 21 2020 at 12:37):

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 (Apr 21 2020 at 12:39):

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

Mario Carneiro (Apr 21 2020 at 12:44):

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 (Apr 21 2020 at 12:45):

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

Bhavik Mehta (Apr 21 2020 at 12:47):

Cool thanks all!


Last updated: Dec 20 2023 at 11:08 UTC