RFC: Bundle of widget improvements

[Vtec234]

Proposal

• This RFC proposes a bundle of improvements to user widgets that I identified over the year from bug reports to ProofWidgets4, as well as my own usage.

• Generalize basic widget declarations.

  • Motivation. When designing user-widgets, our original understanding of "widget" was roughly as "something that could be displayed in the infoview next to the tactic state". With ProofWidgets it became clear that this isn't general enough; for instance, it is useful to be able to declare widgets that are merely subcomponents (for instance, a single button) to be used in other components but which shouldn't be displayed at the top-level.
  • Thus we generalize "user widget" which has a mandatory user-visible name (under the assumption that it will be shown at the top-level) to "widget module" which is just an arbitrary JS module. We now call JS module that produce a React component suitable for top-level display "panel widgets".
  • Implementation.
    • Deprecate Widget.UserWidgetDefinition in favour of Widget.Module which does not require a name field.
      • In pictures, before the change the widget writer controls the blue box and the string contents of the title. After the change, they control the orange box.
    • Deprecate the @[widget] attribute in favour of a @[widget_module] attribute.
    • Rename ofUserWidget to ofPanelWidget to clarify when panel widgets are being used, and other definitions accordingly. (This change was abandoned.)

• Allow storing RPC references in widget props.

  • Motivation. Panel widget nodes in the infotree currently cannot store RPC references, which limits what can be expressed and necessitates various hacks.
  • Implementation. RpcEncodable data can now be stored in ofUserWidget: Vtec234@f7e8c08#diff-513721adf31ab2bf9c9bd846073e7d71720d0f67cef2bbb81a76887071c703daR110-R115

• Add ability to display a widget everywhere (global), and everywhere within a given file (local).

  • Motivation.
    • Users want to be able to declare a widget as always-on within a given file, or when a given namespace is open: e.g. a geometry widget popping up after open GeometryLib. See also Showing a panel widget globally leanprover-community/ProofWidgets4#5.
  • Implementation.
    • Add an environment extension that stores the set of widgets to be displayed at a given position. Support both globally (persisted in .oleans) and locally displayed widgets.
    • Vtec234@6004796#diff-1a6eaee5d12ad418d2657e155b36b353081ee0bc8fefbe6628c6ea0779d1258eR125-R154

• Show all widget infos on the cursor's line rather than just those whose span contains the cursor position.

  • Motivation. This was a papercut that necessitated creating syntax with fake ranges, e.g. in Try this!: https://github.com/leanprover/std4/blob/fbaccce68796c678ece7a4ca0f202dcef98d26e3/Std/Tactic/TryThis.lean#L100-L108
  • Implementation. Use the exact same algorithm as for computing the diagnostics at a given line.

• Beneficiaries: Users of widgets, e.g. in mathlib4.

• Maintainability: There is now an extra environment extension, though I was also able to remove one. Overall complexity did not increase significantly.

Community Feedback

Community feedback was gathered largely in-person or in DMs.

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.

[Vtec234]

@Kha I would appreciate your feedback. I am hoping this does not conflict significantly with your new infrastructure.

[Kha]

No reservations from my side :) . It all sounds sensible to me.