From 992226d7d9c1463b8ce231676e51af93a53772b8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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 | 19 +++++++++++++++++--
 2 files changed, 20 insertions(+), 2 deletions(-)

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) => {