Skip to content

Commit

Permalink
Mark documents with lean4 in parallel.
Browse files Browse the repository at this point in the history
  • Loading branch information
gebner committed Mar 25, 2021
1 parent 234fe1b commit 7bcb876
Showing 1 changed file with 2 additions and 4 deletions.
6 changes: 2 additions & 4 deletions src/extension.ts
Original file line number Diff line number Diff line change
Expand Up @@ -46,10 +46,8 @@ export async function activate(context: ExtensionContext): Promise<any> {
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)
Expand Down

0 comments on commit 7bcb876

Please sign in to comment.