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 5, 2024
1 parent d46cfd6 commit 62caf1f
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 2 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@
#755, cc: #722, #725)
- [hover] Show input howto for unicode characters on hover
(@ejgallego, Léo Stefanesco, #756)
- [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
13 changes: 11 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,16 @@ 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 = () =>
window.visibleTextEditors.some((editor) =>
languages.match(CoqSelector.all, editor.document) > 0);

if(active_editors_for_us ())
start();

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

0 comments on commit 62caf1f

Please sign in to comment.