Transparent selection of Expr
presenters
#4
Labels
enhancement
New feature or request
help wanted
Extra attention is needed
user interface
Questions about UI and UX design
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 theExprPresentation
component. Here are two stacked instances ofExprPresentation
: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 replaceInteractiveExpr
and components using it can begin displaying arbitraryExpr
presentations. This may also motivate replacing the default tactic state with a ProofWidgets-based one that uses the betterInteractiveExpr
(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.The text was updated successfully, but these errors were encountered: