release: v1.5.0

JetBrains-Research · Nov 29, 2023 · 070a1d6 · 070a1d6
1 parent 63168cd
commit 070a1d6
Showing 1 changed file with 6 additions and 8 deletions.
diff --git a/src/test/coqLlmInteractionTests/proofView.test.ts b/src/test/coqLlmInteractionTests/proofView.test.ts
@@ -315,21 +315,19 @@ suite('ProofView parseFile tests', () => {
             await client.start();
             const proofView = new ProofView(client, statusItem); 
 
-            assert.ok(window.activeTextEditor);
-            const res = await proofView.parseFile(window.activeTextEditor);
+            const res = await proofView.parseFile(window.activeTextEditor!);
 
             assert.strictEqual(res.length, theorems.length);
             for (let i = 0; i < res.length; i++) {
                 const theorem = theorems[i];
                 const thrRes = res[i];
 
                 assert.strictEqual(thrRes.name, theorem.name);
-                assert.ok(thrRes.proof);
-                assert.strictEqual(thrRes.proof.proof_steps.length, theorem.numOfSteps);
-                assert.strictEqual(thrRes.proof.is_incomplete, theorem.isIncomplete);
-                assert.strictEqual(thrRes.proof.end_pos.end.line, theorem.endPos.line);
-                assert.strictEqual(thrRes.proof.end_pos.end.character, theorem.endPos.character);
-                assert.strictEqual(thrRes.proof.onlyText(), theorem.proof);
+                assert.strictEqual(thrRes.proof!.proof_steps.length, theorem.numOfSteps);
+                assert.strictEqual(thrRes.proof!.is_incomplete, theorem.isIncomplete);
+                assert.strictEqual(thrRes.proof!.end_pos.end.line, theorem.endPos.line);
+                assert.strictEqual(thrRes.proof!.end_pos.end.character, theorem.endPos.character);
+                assert.strictEqual(thrRes.proof!.onlyText(), theorem.proof);
                 assert.ok(rangesEqual(thrRes.statement_range, theorem.statementRange));
             }