Add user widgets tutorial #1407
Conversation
|
Thanks for your contribution! Please make sure to follow our Commit Convention. |
It looks like triple-backtick blocks are possibly prevented within doc comments. However I need this one since it's JS, not Lean. |
|
Maybe one thing we could sneak in to this PR is an |
|
It looks like markdown code blocks within |
| of a widget instance as an instruction for the infoview: "when the user places their cursor here, | ||
| please render the following widget". | ||
|
|
||
| Every widget instance also contains a `props : Json` value. This value is passed as an argument |
There was a problem hiding this comment.
"contains" is a bit vague here. Could you say more about the value's lifetime regarding server and client?
There was a problem hiding this comment.
I left that in but clarified widget instances a little above, is it better? In this case contains just means that wherever a widget instance is stored, we also store props.
There was a problem hiding this comment.
Hah, now I understand why it's a JSON
| @@ -65,31 +63,42 @@ structure RequestContext where | |||
| initParams : Lsp.InitializeParams | |||
|
|
|||
| abbrev RequestTask α := Task (Except RequestError α) | |||
| abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m | |||
There was a problem hiding this comment.
Is this all just for being able to call readDoc inside of run*M instead of outside?
There was a problem hiding this comment.
It's mostly so that we can type the argument to runM as RequestT M. Consequently the code inside can still access the request handler context, and throw request errors rather than only a generic IO.Error. Another way to put it is that it's kind of commuting the request and termelab/meta/command effects.
There was a problem hiding this comment.
Oh I see, it's about exceptions. As you may know I'd like to avoid duplicate exception layers, but I guess that's not realistic here. What error codes other than internalError are you expecting widget handlers to use?
There was a problem hiding this comment.
At least invalidParams for incorrect arguments.
There was a problem hiding this comment.
I had hoped that would be covered by the deserialization, but I guess the param type will not necessarily describe all argument constraints. I'm still not sure if it's worth the (not terribly big) code complication. The RPC interface of a widget should probably be considered private to the widget, so it's unlikely the client code will expect and handle invalidParams specially, no?
There was a problem hiding this comment.
I could definitely see people writing widget-support RPC libraries which can be used by multiple JS codebases, in which case some kind of error handling needs to happen. For example, our own getWidgetSource is now a bit simpler since it can run in CoreM and use all the standard functions rather than accessing parts of the Snapshot data.
Adds a tutorial for user widgets. It is placed in
doc/examples/because that folder seems to get special treatment with Alectryon and I didn't want to otherwise mess with the build setup.Also adds some helpers for
RequestMoperations.Also adds the
include_strmacro as pretty much every user widget needs it, and it seems generally useful.Merge feat: rubiks cube sample leanprover-community/lean4-samples#3There is a cyclic dependency in that this PR providesinclude_strwhich the sample needs.