semantic highlighting for declarations

Stream: lean4

[Calvin Lee]

this is a bit of a silly question but i figured i'd ask

I'm working on a math project, and prefer to keep around a 'theorem'/'lemma'/'corollary' distinction that was present in lean3 and doesn't exist in lean4 anymore.
Luckily, lean4 is great and adding 'corollary' back is easy:

import Lean
macro "corollary" name:ident args:bracketedBinder* ":" t:term ":=" body:term : command =>
  `(theorem $name $args* : $t := $body )

However, when using this I do not get highlighting on the word 'corollary'.
This is because the highlighting for lemma and theorem was provided by my editor, and isn't provided by lean.
This seems like it would be possible, using the @declaration semantic token, and I see references to this token in the lean source. Is there any way we could tag things like def and lemma with the declaration token?
(this would probably be useful for commands in general, like #print)

[Mac Malone]

@Calvin Lee What editor are you using? Keywords like corollary and #print should get semantic highlighting. I know they do in VSCode and EMACS.

[Calvin Lee]

Neovim

i... didn't actually think about binding to @lsp.type.keyword? i thought it would be too noisy

[Calvin Lee]

Specifically you also want to highlight things like protected and noncomputable (command prefices) differently from declarations imo

[Mac Malone]

@Calvin Lee You definitely want semantic highlighting for keyword, since that is the only token type that is easily producible in Lean at the moment. Unfortunately, tagging syntax with other token types is difficult and is really only supported internally on builtin syntax (at least at the moment).

[Calvin Lee]

"internally" as in... vscode? or internal to the lean compiler

[Notification Bot]

A message was moved here from #lean4 > Creating a Lean project by Calvin Lee.

[Mac Malone]

@Calvin Lee "internally" as in the Lean LSP server (with some help from builtin syntax / elaborators).

[Julian Berman]

@Calvin Lee in case you didn't see it, there's a sample setup (for neovim) here: https://github.com/Julian/lean.nvim/wiki/Configuring-&-Extending#semantic-highlighting (if you have issues with it or want to add any caveats obviously feel free)

[Julian Berman]

Needless to say by the way, if you insist on highlighting stuff outside of semantic highlighting you can of course manually tell nvim to highlight something the way you want regardless of the semantic highlighting with a highlight.