From ea7bf9fdccffc1d4c19307a9eefd5f825b3b136e Mon Sep 17 00:00:00 2001
From: Sebastian Reichelt <SebastianR@gmx.de>
Date: Sun, 3 Jan 2021 16:34:08 +0100
Subject: [PATCH] Avoid checking whether proofs are required or not if we don't
 care about the result. fixes #86

---
 src/shared/logics/hlm/checker.ts | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/shared/logics/hlm/checker.ts b/src/shared/logics/hlm/checker.ts
index 295522e4..e3fa06af 100644
--- a/src/shared/logics/hlm/checker.ts
+++ b/src/shared/logics/hlm/checker.ts
@@ -1443,6 +1443,9 @@ export class HLMDefinitionChecker {
   }
 
   private checkMultiGoalProof(object: Object, proof: FmtHLM.ObjectContents_Proof | undefined, parameters: Fmt.ParameterList | undefined, goals: Fmt.Expression[], context: HLMCheckerContext): void {
+    if (!proof && !this.options.warnAboutMissingProofs) {
+      return;
+    }
     if (parameters) {
       if (proof) {
         if (!proof.parameters) {
@@ -1468,8 +1471,7 @@ export class HLMDefinitionChecker {
           object = proof;
         }
         this.checkProofValidity(object, proof, newGoals, context);
-      } else if (this.options.warnAboutMissingProofs
-                 && !newGoals.some((goal: Fmt.Expression) => this.utils.isTrueFormula(goal))) {
+      } else if (!newGoals.some((goal: Fmt.Expression) => this.utils.isTrueFormula(goal))) {
         this.message(object, parameters || !newGoals.length ? 'Proof required' : `Proof of ${newGoals.join(' or ')} required`, Logic.DiagnosticSeverity.Warning);
       }
     });