From 7bcb876a04173599a6346c3032d8ed47a590cb42 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 25 Mar 2021 15:18:30 +0100 Subject: [PATCH] Mark documents with lean4 in parallel. --- src/extension.ts | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/extension.ts b/src/extension.ts index d1df42380..edc5f1769 100644 --- a/src/extension.ts +++ b/src/extension.ts @@ -46,10 +46,8 @@ export async function activate(context: ExtensionContext): Promise { return api } - for (const textDocument of workspace.textDocuments) { - if (textDocument.languageId === 'lean') - await languages.setTextDocumentLanguage(textDocument, 'lean4') - } + await Promise.all(workspace.textDocuments.map(async (doc) => + doc.languageId === 'lean' && languages.setTextDocumentLanguage(doc, 'lean4'))) const client: LeanClient = new LeanClient() context.subscriptions.push(client)