Transparent selection of Expr presenters #4
Description
As also discussed in #2, there can be many ways to present any given Expr. For example, we may choose to view it as LaTeX at one point and as a diagram at another. The UI should provide users with a choice of which view they want to see. This is currently implemented in the ExprPresentation component. Here are two stacked instances of ExprPresentation:
Unfortunately the selection dropdown takes up space (the selection is not transparent) and means that we can't just replace the default InteractiveExpr component with this one. We should find a better UI design which takes up no space next to expressions, so that it can replace InteractiveExpr and components using it can begin displaying arbitrary Expr presentations. This may also motivate replacing the default tactic state with a ProofWidgets-based one that uses the better InteractiveExpr (or backporting enough changes to Lean core to make it work there).
A possible design would be to have a piece of global UI state and a single dropdown in a corner somewhere using which the default Expr presenter to use be chosen. Departures from the default could then perhaps be chosen via a menu appearing in the hover tooltip. Since the default @leanprover/infoview tooltip cannot be modified directly at the moment, some options would be to (A) add functionality to @leanprover/infoview to modify tooltips, or (B) copy the tooltip components over to ProofWidgets and modify them here, or (C) inject modifications dynamically using some JS hacks.