Make LeanClientProvider responsible for opening documents.

Author: gebner

vscode-lean4/src/leanclient.ts

@@ -83,9 +83,6 @@ export class LeanClient implements Disposable {
         this.outputChannel = outputChannel;
         this.workspaceFolder = workspaceFolder;
 
-        this.subscriptions.push(window.onDidChangeVisibleTextEditors((es) =>
-            es.forEach((e) => this.open(e.document))));
-
         this.subscriptions.push(workspace.onDidChangeConfiguration((e) => this.configChanged(e)));
     }
 
@@ -266,7 +263,6 @@ export class LeanClient implements Disposable {
             this.client.outputChannel.show(true);
         });
 
-        window.visibleTextEditors.forEach((e) => this.open(e.document));
         this.restartedEmitter.fire(undefined)
     }
 
@@ -294,10 +290,7 @@ export class LeanClient implements Disposable {
         c2p.asDiagnostics = (diags) => diags.map(d => c2p.asDiagnostic(d))
     }
 
-    private async open(doc: TextDocument) {
-        if (doc.languageId !== 'lean4') {
-            return
-        }
+    async openLean4Document(doc: TextDocument) {
         if (!this.running) return; // there was a problem starting lean server.
 
         if (!this.isSameWorkspace(doc.uri)){

vscode-lean4/src/utils/clientProvider.ts

@@ -67,7 +67,7 @@ export class LeanClientProvider implements Disposable {
                         const client = this.clients.get(path)
                         void client.restart()
                     } else {
-                        void this.ensureClient(this.getDocument(path), version);
+                        void this.ensureClient(this.getDocument(path).uri, version);
                     }
                 }
             } catch {
@@ -102,17 +102,20 @@ export class LeanClientProvider implements Disposable {
         void this.activeClient?.restart();
     }
 
-    didOpenEditor(document: TextDocument) {
+    async didOpenEditor(document: TextDocument) {
         // All open .lean files are assumed to be Lean 4 files.
         // We need to do this because by default, .lean is associated with language id `lean`,
         // i.e. Lean 3. vscode-lean is expected to yield when isLean4Project is true.
         if (document.languageId === 'lean') {
             // Only change the document language for *visible* documents,
             // because this closes and then reopens the document.
-            void languages.setTextDocumentLanguage(document, 'lean4');
-        } else if (document.languageId === 'lean4') {
-            void this.ensureClient(document, null);
+            await languages.setTextDocumentLanguage(document, 'lean4');
+        } else if (document.languageId !== 'lean4') {
+            return;
         }
+
+        const client = await this.ensureClient(document.uri, null);
+        await client.openLean4Document(document)
     }
 
     getClient(uri: Uri){
@@ -123,18 +126,18 @@ export class LeanClientProvider implements Disposable {
         return Array.from(this.clients.values());
     }
 
-    async ensureClient(doc: TextDocument, versionInfo: LeanVersion | null) {
-        let folder = workspace.getWorkspaceFolder(doc.uri);
+    async ensureClient(uri: Uri, versionInfo: LeanVersion | null): Promise<LeanClient> {
+        let folder = workspace.getWorkspaceFolder(uri);
         if (!folder && workspace.workspaceFolders) {
             // Could be that doc.uri.scheme === 'untitled'.
             workspace.workspaceFolders.forEach((f) => {
-                if (f.uri.fsPath && doc.uri.fsPath.startsWith(f.uri.fsPath)) {
+                if (f.uri.fsPath && uri.fsPath.startsWith(f.uri.fsPath)) {
                     folder = f;
                 }
             });
         }
 
-        const folderUri = folder ? folder.uri : doc.uri;
+        const folderUri = folder ? folder.uri : uri;
         const path = folderUri?.toString();
         let  client: LeanClient = null;
         if (this.clients.has(path)) {
@@ -166,18 +169,20 @@ export class LeanClientProvider implements Disposable {
                 this.progressChangedEmitter.fire(arg);
             });
 
+            this.pending.delete(path);
+            this.clientAddedEmitter.fire(client);
+
             if (!versionInfo.error) {
                 // we are ready to start, otherwise some sort of install might be happening
                 // as a result of UI options shown by testLeanVersion.
-                void client.start();
+                await client.start();
             }
-
-            this.pending.delete(path);
-            this.clientAddedEmitter.fire(client);
         }
 
         // tell the InfoView about this activated client.
         this.activeClient = client;
+
+        return client;
     }
 
     dispose(): void {