theia: Undo can fail to restore previous text

On Windows 7.

1 In a new file type int bob 2 Press Ctrl+Shift+LeftArrow, selecting bob 3 Type jim 4 Press Ctrl+Z to Undo

Expected: int bob Observed: int

Workaround: at 2, instead press Press Shift+LeftArrow thrice.

Same in VS Code, FWIW.

Note: github’s manky rendering has extended the code background region looking almost as if a space before jim was included e.g. on Chrome:

There is actually none: