Zulip Chat Archive

Stream: general

Topic: Custom highlighting


view this post on Zulip 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?

view this post on Zulip 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").

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Apr 21 2020 at 12:47):

Cool thanks all!


Last updated: May 14 2021 at 13:24 UTC