feat: user widgets #194
feat: user widgets #194
Conversation
lean4-infoview/src/infoview/info.tsx
Outdated
| <div style={{display: hasMessages ? 'block' : 'none'}}> | ||
| {widgets && widgets.map(widget => | ||
| <div style={{display: hasWidget ? 'block' : 'none'}} | ||
| key={`widget::${widget.widgetSourceId}::${widget.range?.toString()}`}> |
There was a problem hiding this comment.
This is not a unique key, is it?
There was a problem hiding this comment.
Yeah I was assuming multiple widgets with the same widgetid wouldn't be attached to the same point in the document which might be a bad assumption.
also move widgets above messages in info
also refactor error handling in InfoAux.
This means that it doesn't rerender unecessarily
|
There are some merge conflicts due to #226 now. I'm happy to migrate the code here to the new API if you want me to, but maybe it's better if you check out the differences yourself. |
| } | ||
|
|
||
| /** Given a position, returns all of the user-widgets on the infotree at this position. */ | ||
| export function Widget_getWidgets(rs: RpcSessions, pos: DocumentPosition): Promise<UserWidgets | undefined> { |
There was a problem hiding this comment.
I started on the merge, but noticed the following thing: in our RPC calls, sending DocumentPosition actually makes no sense because we always use the URI at which the RPC call was made (so now, the RpcSessionAtPos URI). getInteractiveDiagnostics just takes in a line range, whereas getInteractiveGoals takes the whole TextDocumentPositionParams but the the handler just ignores it. Therefore I think we should change the widget APIs to just take a Position which is a line+character, but no URI. The goal APIs have been around so I guess we should keep them as-is for compat.
There was a problem hiding this comment.
Ok, I made this change everywhere. Can always revert if we decide otherwise.
Introduces arbitrary javascript widgets to Lean 4.
Todo