diff --git a/CHANGES.md b/CHANGES.md index 002ba362..58c2e8f7 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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_... ---------------------------------------------------- diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index c600a556..ffef1396 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -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); }; @@ -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) => {