From 7a96d822b17ae0ec22ac2e206405ecadb5fe7818 Mon Sep 17 00:00:00 2001 From: Patrick Shipe Date: Tue, 14 Sep 2021 13:37:14 -0600 Subject: [PATCH] Restore ability to change options after loading --- src/workerManager.ts | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/workerManager.ts b/src/workerManager.ts index 18ddfed..3fd360f 100644 --- a/src/workerManager.ts +++ b/src/workerManager.ts @@ -13,18 +13,27 @@ export function createWorkerManager( let client: Promise; let lastUsedTime = 0; + const stopWorker = (): void => { + if (worker) { + worker.dispose(); + worker = undefined; + } + client = undefined; + }; + setInterval(() => { if (!worker) { return; } const timePassedSinceLastUsed = Date.now() - lastUsedTime; if (timePassedSinceLastUsed > STOP_WHEN_IDLE_FOR) { - worker.dispose(); - worker = undefined; - client = undefined; + stopWorker(); } }, 30 * 1000); + // This is necessary to have updated language options take effect (e.g. schema changes) + defaults.onDidChange(() => stopWorker()); + const getClient = (): Promise => { lastUsedTime = Date.now();