RFC: revisit error ranges for `by`, `.`, `next`, `case`

I'd like to revisit the error range spans for proof block starting syntax (by, ., next, case).

This is the status quo:

And it is justified as follows:

/--
  Use position of `=> $body` for error messages.
  If there is a line break before `body`, the message will be displayed on `=>` only,
  but the "full range" for the info view will still include `body`. -/

(Until I fixed that in #4528, the dot had the error only on the dot itself.)

I understand that reasoning, but I believe since the introduction of the “unsolved goals” marker and in particular the the gutter decorations in the vscode plugin (https://github.com/leanprover/vscode-lean4/pull/585) the facts have changed: There are now two other visual indicators that make the range visible.

The issue I’d like to improve here is that even I, as arguably an experience lean user, tend to take a few moments to distinguish between “the first tactic has an error” and “the proof block is incomplete”. I assume that for beginners this must be even worse.

Also new features like simp warning on unused arguments (#8901) mean that more tactics would like to make use of the “squiggly line real estate” and get their signals drowned if they happen to be in the first line of a block.

So the proposal here is put the error range on the keyword only (case, next, by, .). Putting this on the first keyword (and not the =>) makes it also visually uniform and (IMHO) easier to grasp.

Of course the fullrange should still include the whole tactic block.

One downside is that users that are using editors that don’t support the gutter decoration have smaller squiggly errors. I’d say we should optimize for vscode, and it’s not that they are completely missing the signal, it’s just less visible (as it was before #4528). And of course they also benefit from not seeing red squiggly lines under an actually successful tactic.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by locating the proof-block handling for by, ., next, and case, then review the range behavior discussed in #4528 and the gutter-decoration context in vscode-lean4 PR #585. Done means diagnostic ranges cover only the keyword while fullrange still covers the entire tactic block, with the editor tradeoff resolved.