Skip to content

Commit

Permalink
Merge pull request #701 from ejgallego/document_request_display
Browse files Browse the repository at this point in the history
[code] Display JSON data for `coq-lsp.document` in new editor.
  • Loading branch information
ejgallego authored May 10, 2024
2 parents c3f0a0e + 740d651 commit 106cf33
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 2 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
-----------------------------
Expand Down
2 changes: 1 addition & 1 deletion editor/code/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@
},
{
"command": "coq-lsp.document",
"title": "Coq LSP: Get document in serialized format, print in console"
"title": "Coq LSP: Display current Coq document in JSON format"
},
{
"command": "coq-lsp.save",
Expand Down
17 changes: 16 additions & 1 deletion editor/code/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import {
WorkspaceConfiguration,
Disposable,
languages,
Uri,
} from "vscode";

import {
Expand Down Expand Up @@ -281,7 +282,21 @@ 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");
Expand Down

0 comments on commit 106cf33

Please sign in to comment.