## 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: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: May 14 2021 at 13:24 UTC