show number of errors in file I'm working on

Stream: lean4

[Kevin Buzzard]

When minimising/debugging during porting I often have a mathlib4 file with errors open in VS Code, and then another scratch file with errors also open. In this situation VS Code displays the total number of errors in both files in the blue line at the bottom. Is there any way of going back to the Lean 3 behaviour of only showing the errors in the current file? I'm often glancing down there to see how far there is to go in the porting file and I'm constantly being confused by this new behaviour: I want the ultimate goal to be 0 errors, not "number of errors in a scratch file which I have open and don't really want to close". If this is not possible I'd like to open an issue asking for this functionality -- where does it go? The Lean 4 VS Code extension?

(another issue: in Lean 3 I was able to switch between things like "compile only the current file" or "compile nothing right now because I am running Lean on the command line for a bit"). Are these ever coming back? Are they still useful in Lean 4?)

[Shreyas Srinivas]

(deleted)