Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
248 stars 25 forks source link

highlights.scm: @boolean -> @constant.builtin.boolean, @repeat -> @keyword.control.repeat #319

Closed josephholsten closed 9 months ago

josephholsten commented 9 months ago

:wave: I'm trying to clean up some of the themes in helix, noticed https://github.com/helix-editor/helix/blob/master/runtime/queries/lean/highlights.scm is the only highlight query using @boolean, everything else uses @constant.builtin.boolean.

The benefit of this is that a helix theme or treesitter color config which defines @constant or @constant.builtin will also apply.

I also notice there is a @repeat, which might make sense as @keyword.control.repeat, unless it's a @function.builtin.

I'm hoping to update https://docs.helix-editor.com/themes.html to something for all treesitter syntax highlighting queries, so I'll probably be back with doc about that ;-)

Julian commented 9 months ago

Hi there! Thanks for the issue.

I'm not sure @constant.builtin.boolean works in neovim -- are you sure it does? At least according to :h treesitter-highlight-groups the examples show @constant.builtin but for boolean they show @boolean.

On the other hand, work on tree-sitter-lean is effectively stalled (on the grammar being too big to use) which means I basically am not actively working on any of those queries unfortunately...

josephholsten commented 9 months ago

Wow, https://neovim.io/doc/user/treesitter.html#treesitter-highlight really doesn't align with the highlight.scm files over in https://github.com/tree-sitter.

For example, https://github.com/tree-sitter/tree-sitter-ruby/blob/master/queries/highlights.scm uses @function.method not @method, @variable.parameter not @parameter. Clearly I am missing some magic here, I'll dig in. Thanks for the reference, that's really useful.

josephholsten commented 9 months ago

BTW, I'm absolutely planning on providing the patch, just wanted to talk before I threw something over the wall. Thanks for the quick feedback.

Julian commented 9 months ago

Closing this given the above, but yeah if there's something here that can help and that also is correct for nvim, obviously happy to merge a PR, just unlikely to look at doing this myself unless tree-sitter-lean becomes viable again! Appreciated though.