From 62caf1f21f251fc9f8655a96214be44881d559a8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 5 Jun 2024 18:41:47 +0200 Subject: [PATCH] [code] Don't start the language client unless there is an active editor 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 --- CHANGES.md | 3 +++ editor/code/src/client.ts | 13 +++++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) 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) => {