search

viperproject / viper-ide

This is the main repository for the Viper IDE extension for VS Code.
Mozilla Public License 2.0
10 stars 11 forks source link

Request: command to clear all Viper diagnostics #411

Open fpoli opened 1 year ago

fpoli commented 1 year ago

When Viper reports a diagnostic, it remains in the VS Code problems tab even after deleting the Viper program. It would be nice to have a "clear diagnostics" command to get rid of all Viper diagnostics (clearing the status bar as well) without having to restart the IDE.

rayman2000 commented 7 months ago

@fpoli There already exists a command "remove diagnostics caused by this file", which removes the diagnostics but does not clear the status bar. To be sure: What you want is for this command to also clear the bar, not for there to be an additional command right?

fpoli commented 6 months ago

Thanks, I didn't know that command. I just tried again. Now, when moving the focus from file A to file B the IDE automatically clears diagnostics generated by the file A. So, it's no longer possible to have leftover diagnostics generated by a deleted file. This was my main issue.

When preparing the laptop before a Viper demo it's usually nice to also clear the status bar. It would be nice to have a command for that, but the benefit is so little that I'd be fine with closing the issue.