diff --git a/CHANGES.md b/CHANGES.md index ae9e5819..d3c8b15e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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_... ---------------------------------------------------- diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index c600a556..89351d3a 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,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) => {