genearlizing @[widget]

Stream: lean4

[Joachim Breitner]

@Edward Ayers , I am thinking about next steps to make by interactive generally usable, and one would be to clean up the handling of geting ESModule code in Lean into the JS world, and unifying that with what the existing widget code does.
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, and could be used for ESModules don't export react components, or that export react components that are not yet full top-level widgets (as is in the case of by interactive).

Could we generalize that to maybe @[infoview_component] (or keep the name, not so important), and add a suitable JS method (maybe to EditorAPI) that allows JS code to get their hands on the imported component, using the hash (or some other identifier)?

I think the code is all there in the widget handling, and “just” needs to be exposed in a reasonably clean way.

Does that make sense?