viperproject/viper-ide

Request: command to clear all Viper diagnostics

Opened this issue · 2 comments

fpoli commented

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

@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

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.