Skip to content

Commit

Permalink
[code] Display JSON data for coq-lsp.document in new editor.
Browse files Browse the repository at this point in the history
This makes more sense than the current command behavior which is not
usable by almost no one.
  • Loading branch information
ejgallego committed May 9, 2024
1 parent e120ed9 commit 13176d0
Show file tree
Hide file tree
Showing 3 changed files with 20 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: Get document data in serialized JSON format, display in new text editor"
},
{
"command": "coq-lsp.save",
Expand Down
18 changes: 17 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,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");
Expand Down

0 comments on commit 13176d0

Please sign in to comment.