Rename operations sometimes produce broken results

[SReichelt]

When renaming identifiers or moving files, this sometimes results in broken file contents.

At the moment, no sequence of actions that reliably triggers the bug is known, but it happens quite frequently. Possibly, the problem only occurs when unsaved files are involved, e.g. it could be triggered by several consecutive rename operations without saving in between.

The cause could be a VSCode bug but may also be related to interaction with the webview.

Relatedly, renaming symbols with high unicode characters produces broken results, but that is most likely a VSCode bug. (Perhaps it can be reproduced in other extensions as well.)