VS Code info view suppress warnings

Stream: general

[Kevin Buzzard]

Is it possible to make the "Info view: Display Messages (Ctrl+Shift+Alt+Enter)" suppress the warning that files are being imported which contain sorries but not suppress any error?

[Mario Carneiro]

that sounds like a lean PR to me

[Bryan Gin-ge Chen]

We could apply a filter to the warnings and errors as we do for the tactic state. I didn't implement this before since I wasn't sure what the UI should be.

[Kevin Buzzard]

I would be happy with anything. I am trying to debug one particular isolated type class inference issue in a project with several errors, and several sorries; I want to isolate the error and not keep having to scroll down through warnings that several other files have sorries and they're being imported. I know this already