generalizing @[widget]

Stream: lean4

[Wojciech Nawrocki]

It seems that the @[widget] annotation isn’t exactly rightly named: It looks like a general mechanism to get ESModule code into the JS world of the infoview,

Insofar as a "widget" is a React component that can be drawn at the top-level in the infoview and has an associated name (which gets displayed in the collapsible header), the attribute name seems correct. The mechanism for storing ESModules in the server and providing a way for the JS side to retrieve them is one level of abstraction lower and works with "widget sources". Have a look here which should hopefully make the difference a bit clearer.

and could be used for ESModules don't export react components, or that export react components that are not yet full top-level widgets

Indeed the widgetSourceRegistry is not at all specific to top-level components; it is nothing more than a hash-addressed String storage. If you want, you can store any data there using widgetSourceRegistry.addEntry (this is what the @[widget] attribute does) and retrieve it using the getWidgetSource RPC call. The reason why we didn't generalize it to generalStringStorage is pretty much just that anyone who needs a storage for things that aren't widget sources (and in particular might have different types than String) can quite easily add it by registering a new environment extension, so no generality is lost. I think the option to generalize is still open, but again it is not very high priority because Lean core already gives you all that you need to store arbitrary data in this way.

(BTW, why does getWidgetSource have to look at the pos? Can’t you have a global widgetSourceRegistry?)

All RPC calls are made relative to a position and we think of them as executing at that position. For example in

-- line 30
@[widget]
def myWidget : UserWidgetDefinition where
  name := "Hello"
  javascript := ...
-- line 35

calling getWidgetSource(myWidgetHash) at line 35 succeeds whereas on line 30 it would fail.

[Joachim Breitner]

Thanks! So are you suggesting to roll my own registry for the sources of the “inner widgets” or reuse widgetSourceRegistry?

[Wojciech Nawrocki]

I would say roll your own, as widgetSourceRegistry is somewhat of an implementation detail and could change, at least in theory. It should not be too difficult to do even just by copying the implementation of widgetSourceRegistry.