From 4c1cdbcc70e3c265ba5ec6729691424d617f8d16 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Tue, 29 Jun 2021 12:22:07 -0700
Subject: [PATCH] fix: initialization loop

---
 vscode-lean4/src/rpc.ts | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/vscode-lean4/src/rpc.ts b/vscode-lean4/src/rpc.ts
index 75309f3bf..de501544d 100644
--- a/vscode-lean4/src/rpc.ts
+++ b/vscode-lean4/src/rpc.ts
@@ -13,7 +13,6 @@ export class Rpc {
             }, 50)
             this.resolveInit = () => {
                 clearInterval(interval as any)
-                sendMessage({kind: 'initialize'})
                 resolve()
             }
         })
@@ -25,8 +24,12 @@ export class Rpc {
 
     // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types
     messageReceived(msg: any): void {
-        if (msg.kind && msg.kind === 'initialize' && this.resolveInit) {
-            this.resolveInit()
+        if (msg.kind) {
+            if (msg.kind === 'initialize') {
+                this.sendMessage({kind: 'initialized'})
+            } else if (msg.kind === 'initialized' && this.resolveInit) {
+                this.resolveInit()
+            }
             return
         }
         const {seqNum, name, args, result, exception} = msg