refactor: preparing for user-widgets and context suggestions#193
refactor: preparing for user-widgets and context suggestions#193gebner merged 10 commits intoleanprover:masterfrom
Conversation
This is a set of refactors that me and @Vtec234 made while working on user widgets and context suggestions. - some docstrings - refactor InteractiveHypothesis => InteractiveHypothesisBundle - refactor: extract HypothesisBundle render to own component. - introduce a `useAsync` hook for use with rpcs - refactor TypePopupContents - InteractiveGoal and InteractiveHypothesisBundle have mvarId? and fvarIds? fields - helper function mapRpcError - helper enum RpcErrorCode - new override of useEventResult - fix a bug in handleInsertText where it was doing reference eq instead of string eq. Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
EdAyers
force-pushed
the
widget-refactor-pr
branch
from
d49ab07 to
74bacc8
Compare
lean4-infoview/src/components.tsx
Outdated
| }, [pos.character, pos.line, pos.uri, msg]) | ||
|
|
||
| if (tt) return <InteractiveMessage pos={pos} fmt={tt} /> | ||
| else return <></> |
There was a problem hiding this comment.
| else return <></> | |
| else return <>...</> |
| // Update state so the next render will show the fallback UI. | ||
| return { error: error.toString() }; | ||
| } | ||
|
|
There was a problem hiding this comment.
I'm not sure how this component is going to be used (it's still unused). The Lean 3 version had a componentDidCatch handler, should we add this here as well?
There was a problem hiding this comment.
componentDidCatch is needed if you want to log errors. I added a stub that does nothing in case react is looking for that method.
| private async sessionAt(uri: DocumentUri): Promise<RpcSession | undefined> { | ||
| if (this.#connected.has(uri)) return this.#connected.get(uri) | ||
| else if (this.#connecting.has(uri)) return this.#connecting.get(uri) | ||
| else if (this.#connecting.has(uri)) return await this.#connecting.get(uri) |
There was a problem hiding this comment.
The await shouldn't be required here, or am I missing something?
There was a problem hiding this comment.
Hmm I'm not sure. If you do return p where p : Promise<T> in an async function does the compiler automatically squash the Promise<Promise<T>> to a Promise<T>? I guess it must do.
There was a problem hiding this comment.
It's not required, I just put it in for clarity.
lean4-infoview/src/infoview/util.ts
Outdated
| /** This hook will run the given promise function whenever the deps change. | ||
| * There will only ever be one in-flight promise at a time. If the deps | ||
| * change while a promise is still in-flight, then the function will be run | ||
| * again after the first promise has resolved. |
There was a problem hiding this comment.
The purpose of this function is to prevent race conditions where the RPC requests return in a different order than they were sent, right?
- Request 1 is sent with, say, line=42.
- Request 2 is sent with line=90.
- Request 2 returns with diags=[].
- Request 1 returns with diags=['error'].
And withoutuseAsyncwe would now return the diagnostics for line 42 even though we're at line 90.
If that's the case, then that should be written in the docstring.
Is there a reason for "only ever be one in-flight promise at a time"?
There was a problem hiding this comment.
The reason for only having one at a time is so that you don't spam server with requests but maybe the server can handle it.
There was a problem hiding this comment.
Instead of the 'one at a time' model we could instead have the callback of the promise check whether it has been superceded by a later rpc call and discard its result. That would also work.
There was a problem hiding this comment.
It might be worth it to check if the more eager (multiple requests) approach increases responsiveness or not.
There was a problem hiding this comment.
I added an unthrottled version, not sure what the best way to test is. They both seem to work.
There was a problem hiding this comment.
Let's just stick with the unthrottled one for now.
3 participants
This is a set of refactors that me and @Vtec234 made while working on user widgets and context suggestions.
useAsynchook for use with rpcsCo-authored-by: @Vtec234