Skip to content

Conversation

@Vtec234
Copy link
Member

@Vtec234 Vtec234 commented Jan 22, 2026

Adds support for cancelling LSP and RPC requests in infoview code (including widgets). No changes to Lean are needed since the server already handles $/cancelRequest, and RequestM includes checkCancelled.

Main changes:

  • Add an optional AbortSignal argument to LSP and RPC calls. Aborting causes the request to be cancelled which sets the RequestContext.cancelTk at the server end.
  • Split EditorApi into a serializable EditorRpicApi and a (non-serializable) EditorApi wrapper for use in the infoview. This is necessary because AbortSignal cannot simply be sent over to the editor.
  • Clean up handling of Disposable subscriptions in infoview.ts a bit.
  • Fix a racy test.

This spun out of leanprover-community/ProofWidgets4#141 which hand-rolls support for cancelling widget requests. However, it is challenging to ensure that computations are cancelled when the infoview closes, for example, without changing the extension. I also think it is better to use builtin mechanisms already present in RequestM than to implement our own.

@Vtec234 Vtec234 requested a review from mhuisi January 22, 2026 21:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant