Adjusting error ranges for `by`, etc (RFC #8919)

Stream: lean4 dev

[Aaron Hill]

I'm interested in working on https://github.com/leanprover/lean4/issues/8919 . Based on my current understanding, implementing this is going to require:

1. Adjusting Lean.MonadRef (and all of the structures which implement it) to additionaly store something like fullRef: Option (m Syntax). This will be used to store the 'full' Syntax associated with a message - in the by example, this will be the entire by ... expression, while ref will start storing just the by token.
2. Remove BaseMessage.keepFullRange, and instead store fullPos/endFullPos positions (which will be populated from the new fullRef from Lean.MonadRef)
3. Adjust msgToInteractiveDiagnostic to directly construct range and fullRange from pos/endPos and fullPos/endFullPos respectively. This function will no longer ever perform truncation of ranges that span more than one line.

Does that sound correct? I'm unsure about exactly what the API for getting/setting fullRef should like - I assume that we'll want to make it difficult to accidentally update either ref/fullRef without explicitly setting or clearing the other.

[Marc Huisinga]

Your plan is good, but since this will require fairly deep changes to multiple components (including the VS Code extension since the new ranges won't satisfy some invariants that the old ones satisfied), I think that it's best implemented by someone at the FRO at some point.