Feature request: syntactic highlighting for expressions in the InfoView

[ayhon]

I've recently been working on a couple of proofs which use definitions that, when unfolded, include pretty big pieces of code. Parsing them has been a bit complex, and while I don't believe that syntax highlighting would fix the issue, I've certainly been missing it when reading the goals.

While wondering how easy it'd be to implement, I figured I might as well ask for the feature.

[ayhon]

As a motivating example

Actual goal	With syntax highlighting

[iamrecursion]

I'll definitely add my +1 for this feature request. I've been working with some big proofs too that I could definitely get some use of syntax highlighting in the infoview for.

[lucianchauvin]

Is there syntax highlighting in the InfoView in VS Code?

[Julian]

Sorry, I thought I'd responded to this -- I've also thought about this before but as far as I know it's not possible to do this in Neovim today. Or specifically, it's only really feasible to do with tree-sitter, and we just don't have anything near a fully working tree-sitter parser. But using vim syntax highlighting or LSP semantic tokens (both of which we obviously do have) it's not possible to do this for arbitrary regions in a buffer not of filetype lean.

Happy to hear if anyone has ideas though or to leave this open, maybe someday I'll be able to get tree-sitter-lean working.

[iamrecursion]

I keep wondering about writing a Tree Sitter grammar for Lean from scratch, but I don't know why the existing one was abandoned.

[Julian]

The grammar is gigantic and made tree sitter fall over. I stopped when we hit the GitHub filesize limit and I couldn't figure out how to optimize it back down again. I saw Ada's grammar have similar issues. It's quite possible I was doing something wrong (and I've tried around a year ago to restart from scratch) but yeah it seems non-trivial.

[iamrecursion]

Oh goodness that does sound like a problem, yeah.