diff --git a/CHANGES.md b/CHANGES.md index c1c2616bd..e204c5b81 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -106,6 +106,8 @@ (@ejgallego, @Alizter, #689, #693) - Better types `coq/perfData` call (@ejgallego @Alizter, #689) - New server option to enable / disable `coq/perfData` (@ejgallego, #689) + - The `coq-lsp.document` VSCode command will now display the returned + JSON data in a new editor (@ejgallego, #701) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/editor/code/package.json b/editor/code/package.json index bca67a6b0..d3b000a6a 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -96,7 +96,7 @@ }, { "command": "coq-lsp.document", - "title": "Coq LSP: Get document in serialized format, print in console" + "title": "Coq LSP: Get document data in serialized JSON format, display in new text editor" }, { "command": "coq-lsp.save", diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 81b13204f..cfe11b885 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -13,6 +13,7 @@ import { WorkspaceConfiguration, Disposable, languages, + Uri, } from "vscode"; import { @@ -281,7 +282,22 @@ export function activateCoqLSP( version ); let params: FlecheDocumentParams = { textDocument }; - client.sendRequest(docReq, params).then((fd) => console.log(fd)); + client.sendRequest(docReq, params).then((fd) => { + + // EJGA: uri_result could be used to set the suggested save path + // for the new editor, however we need to see how to do that + // and set `content` too for the new editor. + let path = `${uri.fsPath}-${version}.json`; + let uri_result = Uri.file(path).with({ scheme: "untitled" }); + + let open_options = { + language: "json", + content: JSON.stringify(fd, null, 2), + }; + workspace.openTextDocument(open_options).then((document) => { + window.showTextDocument(document); + }); + }); }; const trimNot = new NotificationType<{}>("coq/trimCaches");