Fetch source code from Lean and dynamically import it as a JS module.
The source must hash to hash (in Lean)
and must have been annotated with @[widget] or @[widget_module]
at some point before pos.
If hash does not correspond to a registered module,
the promise is rejected with an error.
Experimental import support for widget modules
The module may import other @[widget_module]s by hash
using the URI scheme 'widget_module:hash,<hash>'
where <hash> is a decimal representation
of the hash stored in Lean.Widget.Module.javascriptHash.
In the future,
we may support importing widget modules by their fully qualified Lean name
(e.g. 'widget_module:name,Lean.Meta.Tactic.TryThis.tryThisWidget'),
or some way to assign widget modules a more NPM-friendly name
so that the usual URIs (e.g. '@leanprover-community/pro-widgets') work.
Fetch source code from Lean and dynamically import it as a JS module.
The source must hash to
hash(in Lean) and must have been annotated with@[widget]or@[widget_module]at some point beforepos.If
hashdoes not correspond to a registered module, the promise is rejected with an error.Experimental
importsupport for widget modulesThe module may import other
@[widget_module]s by hash using the URI scheme'widget_module:hash,<hash>'where<hash>is a decimal representation of the hash stored inLean.Widget.Module.javascriptHash.In the future, we may support importing widget modules by their fully qualified Lean name (e.g.
'widget_module:name,Lean.Meta.Tactic.TryThis.tryThisWidget'), or some way to assign widget modules a more NPM-friendly name so that the usual URIs (e.g.'@leanprover-community/pro-widgets') work.