fix: incremental goal state requests select incomplete snapshot

[mhuisi]

This PR fixes a bug where the goal state selection would sometimes select incomplete incremental snapshots on whitespace, leading to an incorrect "no goals" response. Fixes #6594, a regression that was originally introduced in 4.11.0 by #4727.

The fundamental cause of #6594 was that the snapshot selection would always select the first snapshot with a range that contains the cursor position. For tactics, whitespace had to be included in this range. However, in the test case of #6594, this meant that the snapshot selection would also sometimes pick a snapshot before the cursor that still contains the cursor in its whitespace, but which also does not necessarily contain all the information needed to produce a correct goal state. Specifically, at the InfoTree-level, when the cursor is in whitespace, we distinguish competing goal states by their level of indentation. The snapshot selection did not have access to this information, so it necessarily had to do the wrong thing in some cases.

This PR fixes the issue by adjusting the snapshot selection for goals to explicitly account for whitespace and indentation, and refactoring the language processor architecture to thread enough information through to the snapshot selection so that it can decide which snapshots to use without having to force too many tasks, which would destroy incrementality in goal state requests.

Specifically, this PR makes the following adjustments:

• Refactor SnapshotTask to contain both a Syntax and a Range. Before, SnapshotTasks had a single range that was used both for displaying file progress information and for selecting snapshots in server requests. For most snapshots, this range did not include whitespace, though for tactics it did. Now, the reportingRange field of SnapshotTask is intended exclusively for reporting file progress information, and the Syntax is used for selecting snapshots in server requests. Importantly, the Syntax contains the full range information of the snapshot, i.e. its regular range and its range including whitespace.
• Adjust all call-sites of SnapshotTask to produce a reasonable Syntax.
• Adjust the goal snapshot selection to account for whitespace and indentation, as the InfoTree goal selection does.
• Fix a bug in the snapshot tree tracing that would cause it to render the Info of a snapshot at the wrong location when trace.Elab.info was also set.

This PR is based on #6329.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-12 15:17:56)