Trimming whitespace fix

[raulTUe]

Description

This is a pull request to partially solve the trimming whitespace issue. We now reload the editor only if the file has changed on save, and always give a warning to the user when the trim trailing whitespace setting is on.

Changes

The editor effectively re-initializes if the underlying file has changed when the file was saved, which only really occurs when the trim trailing whitespace setting is on. This makes it clunky if auto save is on, but the warning should prevent this.

Testing this PR

When initializing the extension, the warning should appear on the bottom left of the screen. Moreover, if you turn on trim trailing whitespace setting, and then add a couple of spaces at the end of one of the input areas, and press ctrl+s, then the editor will flash and reinitialize.

[raulTUe]

With this implementation there still seems to be a bug when saving files with the trim whitespace setting on:

1. Open the tutorial and go to the first input area.
2. Type Test. (mind the trailing spaces).
3. Hit Ctrl-S to save and hence refresh the document.
4. Click again in the same input area, where Test. lies without the trailing whitespace.
5. Hit backspace once, and wait 5 seconds.
6. Try hitting backspace or typing any other letter.
7. Any input in this input area doesn't have any effect.

[sonarqubecloud]

Quality Gate passed

Issues
25 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud