to_additive and DeclarationRange.range

Stream: mathlib4

[Matthew Ballard]

Currently to_additive supplies the declaration range of the syntax to_additive alone (assuming no target in the attribute) for the docs#Lean.DeclarationRanges.range. From the specifications for the LSP, shouldn't it be the whole span including the to_additive attribute and the un-additivized declaration? The current behavior is that docs#DeclarationRanges.selectionRange is the to_additive declaration range so we really don't lose any info.

[Damiano Testa]

I am in favour of this suggestion: I am happy that selectionRange stays just to_additive, and have probably exploited this at some point. I personally have not used the range much, except to answer questions on Zulip about finding declaration ranges! :slight_smile:

[Damiano Testa]

I also have in the back of my mind the idea that at some point a minimizer will appear and, when I thought of implementing it myself, getting the ranges for the additive declarations would have helped.

[Matthew Ballard]

I think "I want the next line after some declaration" is something that should be straightforward to accomplish

[Floris van Doorn]

Sounds good to me. I decided on the declaration range semi-arbitrarily.