diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts index 4a6f7547..c3354aad 100644 --- a/vscode-lean4/test/suite/utils/helpers.ts +++ b/vscode-lean4/test/suite/utils/helpers.ts @@ -135,6 +135,9 @@ export async function initLean4Untitled(contents: string): Promise { - let count = 0 + const totalRetries = retries while (retries > 0) { const text = editor.document.getText() const pos = text.indexOf(word) - if (pos < 0) { - await sleep(delay) - count += 1 - } else { + if (pos >= 0) { return new vscode.Range(editor.document.positionAt(pos), editor.document.positionAt(pos + word.length)) } + await sleep(delay) + retries -= 1 } - const timeout = (retries * delay) / 1000 + const timeout = (totalRetries * delay) / 1000 assertAndLog(false, `word ${word} not found in editor after ${timeout} seconds`) } @@ -541,6 +543,7 @@ export async function clickInfoViewButton(info: InfoProvider, name: string): Pro try { const cmd = `document.querySelector(\'[data-id*="${name}"]\').click()` await info.runTestScript(cmd) + return } catch (err) { logger.log(`### runTestScript failed: ${err.message}`) if (retries === 0) {