Skip to content

Commit

Permalink
[code] Don't start the language client unless there is an active edit…
Browse files Browse the repository at this point in the history
…or for us

This seems like the right setup, making the server start lazy.

Still it would be better that VSCode API allowed us to activate our
extension in a more fine-grained fashion.

Fixes #750
  • Loading branch information
ejgallego committed Jun 6, 2024
1 parent d5b1b39 commit 992226d
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 2 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,9 @@
it is often not perfect. (@ejgallego, #762, fixes #317)
- [lsp] [hover] Show full name and provenance of identifiers
(@ejgallego, #762)
- [code] Don't start server on extension activation, unless an editor
we own is active. We also auto-start the server if a document that
we own is opened later (@ejgallego, #758, fixes #750)

# coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
----------------------------------------------------
Expand Down
19 changes: 17 additions & 2 deletions editor/code/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -460,7 +460,7 @@ export function activateCoqLSP(
0
);
lspStatusItem.command = "coq-lsp.toggle";
lspStatusItem.text = "coq-lsp (activating)";
lspStatusItem.text = "coq-lsp (not active)";
lspStatusItem.show();
context.subscriptions.push(lspStatusItem);
};
Expand Down Expand Up @@ -521,7 +521,22 @@ export function activateCoqLSP(

createEnableButton();

start();
// Fix for bug #750
//
// XXX we need to keep an eye to start the client if a buffer that
// belongs to us is open.
const active_editors_for_us = (editors: readonly TextEditor[]) =>
editors.some(
(editor) => languages.match(CoqSelector.all, editor.document) > 0
);

window.onDidChangeVisibleTextEditors((editors) => {
if (!client || !client.isRunning()) {
if (active_editors_for_us(editors)) start();
}
}, context.subscriptions);

if (active_editors_for_us(window.visibleTextEditors)) start();

return {
goalsRequest: (params) => {
Expand Down

0 comments on commit 992226d

Please sign in to comment.