Request: Formatter to emit proven fine-grained edits

[MikaelMayer]

In the PR #2399, formatting on the IDE results in an action that wipes out entirely the previous text and inserts the formatted program.
It would be great to actually transform the formatter in Dafny to emit a diff such that we prove that applying the diff provides the same output, and we can then emit that diff instead of a single change.
Benefits

• (to confirm) previous verification can be kept intact.

See function GetTextEditToFormatCode in the LSP.