Add warning message when global and workspace TLC options set

[klinvill]

Adds on to #207 by adding a warning message (that can be silenced) informing users when they have both global and workspace settings for TLC options. In this case the workspace settings will take precedence. An example warning message is shown below.

This PR addresses the following concern:

the extension behavior will be confusing in the following scenario:

• The user runs a model check, provides some options.
• The user goes to global settings and changes the default options for TLC.
• The user runs a model check, and the extensions shows the prompt with the same options he or she provided on the step 1, with no respect to the new global settings.

[lemmy]

FWIW: To me, this is another indicator that TLC options shouldn't be stored as workspace or global settings.

[sonarqubecloud]

Kudos, SonarCloud Quality Gate passed!

0 Bugs
0 Vulnerabilities
0 Security Hotspots
0 Code Smells

No Coverage information
0.0% Duplication

[lemmy]

• Why not include the global config value in the warning dialog (the workspace one will be shown in the prompt)?
• Why not extend the warning to other settings such as CFG_JAVA_OPTIONS, CFG_PLUSCAL_OPTIONS, ... ?

@alygin I propose to make @klinvill a committer.

[klinvill]

* Why not include the global config value in the warning dialog (the workspace one will be shown in the prompt)?

I'd prefer not to show the value since it's pretty easy to find what the current value is set to in the settings window, and since longer configs clutter up the message window. It'll be an easy change though if folks disagree.

* Why not extend the warning to other settings such as `CFG_JAVA_OPTIONS`, `CFG_PLUSCAL_OPTIONS`, ... ?

I think that's an excellent suggestion. I moved the warning functionality into the getConfigOptions() function which looks like is generally used to fetch configurations. I'm still relying on a single global supressConfigWarnings variable, so suppressing the warning message for CFG_JAVA_OPTIONS will also suppress it for CFG_TLC_OPTIONS, but I think that's preferable to having to silence it once for each different configuration.

alygin I propose to make klinvill a committer.

Thanks for the proposal. Unfortunately I'm not using TLA+ as much these days so I likely will not be very active, but I'm happy to help out a bit (especially for the features I've added)!

[lemmy]

IMO, clutter should be minimized for frequently appearing message (warning) dialogs. Do we expect this warning to appear frequently? I'm also not sure if novice (VSCode) users will know where to find the settings. Ideally, the warning would have a clickable link. :-)

I don't think we need to silence this warning for all configs.

[lemmy]

alygin I propose to make klinvill a committer.

Thanks for the proposal. Unfortunately I'm not using TLA+ as much these days [...]!

:-(

[klinvill]

I like the idea of a clickable link! I added one in to the the latest commit. Here is what it currently looks like:

I also took a look at what it would look like if we added the global value to the warning. It doesn't look as cluttered as I was expecting, but I still personally prefer the message without the global value. I agree though that it should be an infrequent message and am fine adding in the global value if you still think it's the best way to proceed.

[sonarqubecloud]

Kudos, SonarCloud Quality Gate passed!   

0 Bugs
0 Vulnerabilities
0 Security Hotspots
1 Code Smell

No Coverage information
0.0% Duplication

[lemmy]

Looking at the second dialog, it would be better to show the workspace configuration value because this is what the default (ok) will be. Minor; use italics for the actual value?

Never mind, I should have read my own comment: #208 (comment)

[klinvill]

Looking at the second dialog, it would be better to show the workspace configuration value because this is what the default (ok) will be.

The workspace configuration value is displayed in the configurations prompt (when running the model checking) so the user should still be able to see what the workspace config is.

Minor; use italics for the actual value?

It looks like formatting text in messages is blocked on this issue: microsoft/vscode#54272. A previous issue said some basic markdown formatting should work, but I wasn't able to get it to work when I tried it myself. I believe the limited markdown support was probably removed at some point in the past.

[lemmy]

LGTM

[lemmy]

@klinvill By the way, have you seen the Github invite to join this repo?

[klinvill]

@lemmy I saw an invite come across from alygin, but unfortunately when I tried to accept it (about a week and a half ago, before it expired) I saw a message that "This invitation is invalid". He thought I could be seeing the error because the repo had been transferred over to the TLAPlus organization. Are you able to send a new invite?

[lemmy]

@klinvill Did you get a new invite?

[klinvill]

@lemmy yup, and looks like that one worked. Thanks!