RFC: deselect all in info view

[PatrickMassot]

Proposal

It would be nice to have an action to de-select everything in the info view, hopefully with an assigned default key-binding.

Currently this is not crucial. But several people are working on point and click interfaces that will propose tactics to run based on what is currently selected. The calc widget in Mathlib already does that. In this context it is nice to click around to see propositions but going back is slightly painful.

Community Feedback

See discussion on Zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.