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