Get proof blocks api #960
Merged
Get proof blocks api #960
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This will allow to create an api so that outside extensions can query the document and get a structured view of the proofs it contains.
Now extensions that depend on vscoq can get all the document proofs.
rtetley
force-pushed
the
get-proof-blocks-api
branch
from
431d806 to
0b05cfb
Compare
gares
reviewed
Dec 9, 2024
| @@ -284,6 +301,9 @@ module Request = struct | |||
| | "vscoq/documentState" -> | |||
| let+ params = Lsp.Import.Json.message_params params DocumentStateParams.t_of_yojson in | |||
| Pack (DocumentState params) | |||
| | "vscoq/documentProofs" -> | |||
| let+ params = Lsp.Import.Json.message_params params DocumentProofsParams.t_of_yojson in | |||
| Pack (DocumentProofs params) | |||
There was a problem hiding this comment.
I'm wondering if we can easily version these custom queries, eg "vscoq/documentProofs/v1" so that we can update the format later without necessarily breaking badly the plugins that use this extension
There was a problem hiding this comment.
So after thinking about it, we make it accessible through a function in the client. If we need new versions it should be easy to keep everything wired on our end when plugins use our extension.
cas-haaijman
reviewed
Dec 9, 2024
client/src/extension.ts
Outdated
| const params: DocumentProofsRequest = {textDocument}; | ||
| const req = new RequestType<DocumentProofsRequest, DocumentProofsResponse, void>("vscoq/documentProofs"); | ||
| Client.writeToVscoq2Channel("Getting proofs for: " + uri.toString()); | ||
| client.sendRequest(req, params).then( |
There was a problem hiding this comment.
This promise should probably be returned
rtetley
force-pushed
the
get-proof-blocks-api
branch
from
8a582b4 to
a3b30ba
Compare
Before we would only add new sentences during the parsing phase, which works on the first parsing but leads to unwanted behaviors after an edit.
If the document is parsing, the document should resend the documentProofs request later.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR aims at exposing an API which will allow extensions to query the document and get proof blocks in a structured view. This can be useful for a number of users who which to build an extension to vscoq.
Down the line we also ended up fixing an outline bug, in which symbols were never removed but always added.