From fa2af935f874884f70e14e7b6ca8a95721a657b0 Mon Sep 17 00:00:00 2001 From: Ruben Fiszel Date: Fri, 29 Jul 2022 01:45:53 +0200 Subject: [PATCH] monaco-lsp fixes --- frontend/src/lib/components/Editor.svelte | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/frontend/src/lib/components/Editor.svelte b/frontend/src/lib/components/Editor.svelte index f839fd7dc4..b172d3b662 100644 --- a/frontend/src/lib/components/Editor.svelte +++ b/frontend/src/lib/components/Editor.svelte @@ -34,7 +34,7 @@ export let extraLib: string = '' export let extraLibPath: string = '' - let websockets: MonacoLanguageClient[] = [] + let websockets: [MonacoLanguageClient, WebSocket][] = [] let websocketInterval: NodeJS.Timer | undefined let lastWsAttempt: Date = new Date() let nbWsAttempt = 0 @@ -165,7 +165,7 @@ const reader = new WebSocketMessageReader(socket) const writer = new WebSocketMessageWriter(socket) const languageClient = createLanguageClient({ reader, writer }, name, options) - websockets.push(languageClient) + websockets.push([languageClient, webSocket]) languageClient.start() lastWsAttempt = new Date() @@ -284,7 +284,8 @@ async function closeWebsockets() { for (const x of websockets) { try { - await x.stop() + await x[0].stop() + x[1].close() } catch (err) { console.log('error disposing websocket', err) }