When InfoView has many hypotheses, users have to scroll a lot to examine them. In particular some hypothesis are multil-line taking a lot of screen space. It would be nice if we could collapse multi-line hyps into one line when needed, similar to how it is done for goals (via a clickable triangle control next to the name).
FYI: this is what we have in proof-general model in Emacs for Coq, and I found it very handy.
When InfoView has many hypotheses, users have to scroll a lot to examine them. In particular some hypothesis are multil-line taking a lot of screen space. It would be nice if we could collapse multi-line hyps into one line when needed, similar to how it is done for goals (via a clickable triangle control next to the name).
FYI: this is what we have in proof-general model in Emacs for Coq, and I found it very handy.