Getting range information from the server

Stream: lean4

[Julian Berman]

I want to implement nice Lean text objects for lean.nvim. For non-vim users this means basically "nice ways to select parts of the file which are in some way a related editable unit".

Specifically the first 2 obvious ones (because of how useful they'd be) are "the entire current Lean declaration surrounding the cursor" and "the current tactic surrounding the cursor" -- in order to do this well though I ideally would have the server tell me what those line/columns are rather than trying to parse things on the client side. @Marc Huisinga have you thought about this sort of thing at all / do you have any plans here perhaps / is there something that even exists already that I'm forgetting about?

[Eric Wieser]

I think there's some "selection ranges" api in the LSP?

[Julian Berman]

Yeah I know that exists in LSP -- I don't know whether it has any "semantic" meaning

[Julian Berman]

I think it might just be "give me a list of ranges" -- but I'm not sure whether you can specify some semantic range you care about (which you'd need for the examples above) (I guess I'll go read)