highlighting of custom notation

Stream: lean4

[MangoIV]

Hi, I have notation like
scoped notation:50 a " has " b:51 " in " c => ... and I see that in gets highlighted, probably because of the List in, but has doesn't. Do I have to implement highlighting for every word? If so how? If not, how does this work?

[Kyle Miller]

Assuming you're using VS Code: There are some keywords built into the VS Code extension, which probably explains "in". Make sure you have "semantic highlighting" enabled: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Manual.20syntax.20highlighting.20in.20VS.20Code/near/373188215

[MangoIV]

I’m using neovim, so I will have a look whether something equivalent exists there

[Kyle Miller]

It looks like @Julian Berman has some tips: https://github.com/Julian/lean.nvim/wiki/Configuring-&-Extending#semantic-highlighting

[MangoIV]

This looks useful, will try it out tomorrow

[MangoIV]

Seems like it changes nothing for me :3 Perhaps it was already on

[Julian Berman]

I see
Screenshot-2023-08-27-at-07.58.41.png

(with semantic highlighing enabled). Do you see something different?

[MangoIV]

Yes, the has is highlighted differently than the in. Can you perhaps link me to your neovim config, please?

[Julian Berman]

Everything is here: https://github.com/Julian/dotfiles/

[Julian Berman]

(I can try to point you more specifically tomorrow if need be)

[MangoIV]

Thank you I will try it out and will come back if I’m too stupid again :3