highlighting unused segments in a proof

Stream: lean4

[Roozbeh Yousefzadeh]

Hello, In VS Code, I used to see the unused/unnecessary segments in the proofs highlighted with some bright color. I don't see those highlights anymore. Is there some way that I can bring back such automatic highlighting? Thanks.

[Sebastian Ullrich]

You may be referring to the option linter.unusedVariables.analyzeTactics that now defaults to false, see its description for some caveats

[Roozbeh Yousefzadeh]

This is it! Thank you so much!