Bhakti Shah (Mar 07 2023 at 14:27): Bhakti Shah (Mar 07 2023 at 14:27):Is the command Get document in serialized format, print in console currently functional in the vscode extension, or is it a placeholder? I'm seeing server events but not actually seeing the output in the console.
Emilio Jesús Gallego Arias (Mar 07 2023 at 17:04):Hi @Bhakti Shah , the command is functional, but the console it prints is the dev console
Emilio Jesús Gallego Arias (Mar 07 2023 at 17:04):That you can open with Ctrl-Caps-I
Emilio Jesús Gallego Arias (Mar 07 2023 at 17:04):Maybe we should print in a different console?
Emilio Jesús Gallego Arias (Mar 07 2023 at 17:04):That command is more geared for clients making their own Coq LSP instance
Emilio Jesús Gallego Arias (Mar 07 2023 at 17:04):But I'm very happy to make any changes that would be useful for you
Emilio Jesús Gallego Arias (Mar 07 2023 at 17:04):Next release is just a few days away
Emilio Jesús Gallego Arias (Mar 07 2023 at 17:46):In particular the command is called "Open Webview Developer Tools"
Bhakti Shah (Mar 08 2023 at 03:19):Oh I see - yeah I’ve used that console before, I just assumed it would be the debugger console — thanks! I’ll maybe make a pull request with a printing location that might be more helpful to me
Emilio Jesús Gallego Arias (Mar 08 2023 at 13:14):Yes please!
Bhakti Shah (Apr 16 2023 at 05:03):adding on to this -- i don't think this command is actually working because i don't see anything printed in the debugger console of the window im running the extension from, or in the webview dev tools window in the extension host process
on further debugging i think the promise is actually getting rejected? I modified the code to client.sendRequest(docReq, params).then((fd) => console.log(fd), () => console.log('promise rejected'));
where I'm just printing promise rejected for the onrejected parameter, and i am seeing promise rejected printed initially, but it's not consistently doing that? just for the initial call
it doesn't print the doc either though, which is confusing because it should go into one of the two callback branches at any point of time if my understanding is right
Emilio Jesús Gallego Arias (Apr 18 2023 at 14:02):Oh, indeed we should print a better message when the promise is rejected, the coq-lsp Server Events Window should tell you what the reason was, likely document is not ready. Please open a bug or a PR to improve this.
When a request such as getDocument arrives, coq-lsp will handle it in two possible ways:
Note however that if you edit the document after the request is sent, we reject it as the document is stale. But note that we could do differently and serve the request referring to the old document.
Does it make sense?
I think indeed we could improve getDocument a lot by opening an editor window with the json contents; I'll be happy to give it a go, but feel free to try too.
Last updated: Apr 18 2024 at 23:01 UTC