RFC: Interactions between different widgets

Proposal

It would be nice to give widgets access to some shared state. This would allow some form of communication between widgets.

In Verbose Lean, there is a general suggestion widget that allows to select expressions in the tactic state and get suggestions for a next step. When enabled in an exercise, this widget is always shown in the proof. But there is also a more specialized widget for calc block that is shown when the cursor is inside a calc. The specialized widget needs to switch off the general one, otherwise the UI becomes very confusing.

This is currently done by CSS injection: the specialized widget includes a html style tag that changes the display html property of the general widget. But this is a horrible hack and won’t work in neovim.

One fix would be to allow Lean libraries to define global tactic state variables that widgets could read and write. Verbose Lean would define a global “display general suggestion widget” flag, with initial value true. The general suggestion widget would read that flag before deciding to emit anything (or alternatively the exercise elaborator would read it) and the specialized calc widget would set it to false.

Community Feedback

Wojciech told me there is currently no way to do that. Marc asked to create a brief RFC here.

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.

Start by reviewing the general suggestion widget and the specialized calc widget described in the proposal, including their current CSS-injection interaction. Determine the project-supported mechanism for shared widget state and define how the general widget can be suppressed in both the browser UI and Neovim; the RFC is complete when that design is agreed and actionable.