filter Lean messages

Stream: general

[Patrick Massot]

@Gabriel Ebner it would be nice to add a button next to the "Updating/Stopped" toggle which would allow filtering out certain context lines, especially everything starting with _inst_. Because of mixin classes, I currently work on a proof whose starting context goes up to _inst_24. Very quickly I need to scroll down to see the current goal...

[Patrick Massot]

An even more aggressive option would be to also filter out .* : Type .*

[Patrick Massot]

We could have a toggle cycling between default (show every line), filter out instances, filter out instances and types.