User configuration is buggy

[a1994846931931]

Description

Summary:

1. Change of user configuration doesn't take effect
2. Editor of the user configuration is buggy

1. Change of user configuration doesn't take effect

Change Workspace Configuration (good - takes a while to take effect though):

Change User Configuration (buggy):

2. Editor of the user configuration is buggy

"Add Value" Doesn't Refresh the Editor

Editor's Weird Behaviour

Notice how the user configuration editor becomes dirty every time I click on it. It only happens with "editor.formatOnSave" on. In addition, the font size configuration doesn't affect user configuration editor.

Reproduction Steps

See gifs.

OS and Theia version:
OS: Ubuntu 18.04
Theia: 4852766

Diagnostics:

[akosyakov]

@a1994846931931 workspace settings are overriding user settings, are you sure that workspace settings don't contain editor.formatOnSave when you edit user settings?

[a1994846931931]

@a1994846931931 workspace settings are overriding user settings, are you sure that workspace settings don't contain editor.formatOnSave when you edit user settings?

@akosyakov Do you mean in "Editor's Weird Behaviour"? Yes, it does. The workspace settings contain editor.formatOnSave, and it's set to true.

[akosyakov]

@a1994846931931 oh, sorry, i meant editor.fontSize and Change User Configuration (buggy):. It looks like an event is missing, we have a good coverage of tests for resolving preferences but not emitting change events.

[a1994846931931]

@a1994846931931 oh, sorry, i meant editor.fontSize and Change User Configuration (buggy):. It looks like an event is missing, we have a good coverage of tests for resolving preferences but not emitting change events.

@akosyakov No. As you can see in the gif, I've deleted settings.json ( thus no Workspace is shown in Preferences widget ) before testing on user configuration.

[colin-grant-work]

I'm unable to reproduce this behavior after #7105.