More Info customization

[JasonGross]

Is your feature request related to a problem?

Currently Info is parameterized by "levels of unfolding", which doesn't work well if tactic depth does not match abstraction level.

Proposed solution

I propose that Info could also take whitelists or blacklists of tactics to unfold in the display.

Alternative solutions

More fine-grained control is also possible, for example by allowing a tree of nested whitelist/blacklists, e.g., "in this tactic unfold intuition, but in this other tactic don't"

Additional context

Zulip

[ejgallego]

That's a good idea, tho for most users I have for traces these days (UI and ML folks), indeed they'd be served better by the full structure and some client-side filtering, but YMMV . I cc @afwd as she's been working on Info so she's aware of the Zulip discussion.