tactic state filtering in VS code

Stream: general

[Bryan Gin-ge Chen]

Recently, a Lean user "ratmice" requested a feature for the VS code extension which could show/hide variables beginning with _ from the tactic state in the info view. @Patrick Massot suggested that a general filtering feature could be useful. So, I threw together a "tactic state filtering" PR for the VS code extension. Currently the PR adds a dropdown menu to the info view window which displays a customizable list of filters which can be applied (either "positively" or "negatively") to the tactic state.

While this does the job, I think it might not be too hard to make the filtering more interactive, e.g. so that you could click on x's next to particular items in the tactic state to hide them. See the PR thread for a more specific proposal. I'd like to get more feedback before I write more code. What would you like to see from a "filtering" feature?

[Johan Commelin]

This sounds really good. I can't currently test it... but this is is something I've wished for quite a long time.