From 8db0436975f0377f5dde8b4d5e46edd2c8eaba9e Mon Sep 17 00:00:00 2001
From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com>
Date: Wed, 29 Sep 2021 17:11:37 +0200
Subject: [PATCH] Actually fix exception thrown by last example

---
 .../latexcreator/ExplanationCreator.java        | 17 ++++++++++-------
 .../ExplanationCreatorUnification.java          | 14 ++------------
 2 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java
index 35884ea..ff5d7d4 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java
@@ -193,13 +193,16 @@ public class ExplanationCreator implements StepVisitor {
         explanationTexts.add(createLatexLetStep(letD, variable, innerTerm, variableDefinition));
 
         letD.getTypeInferer().getFirstInferenceStep().accept(this);
-        ExplanationCreatorUnification unification =
-                new ExplanationCreatorUnification(letD.getTypeInferer(), locale, provider, MODE, letCounter, true,
-                        Optional.of(variable));
-        explanationTexts.addAll(unification.getUnificationsTexts().getLeft());
-        errorOccurred = unification.getUnificationsTexts().getRight();
-        letCounter--;
-
+        // skip creation of unification texts if nested let produced an error
+        if (!errorOccurred) {
+            ExplanationCreatorUnification unification =
+                    new ExplanationCreatorUnification(letD.getTypeInferer(), locale, provider, MODE, letCounter, true,
+                            Optional.of(variable));
+            explanationTexts.addAll(unification.getUnificationsTexts().getLeft());
+            errorOccurred = unification.getUnificationsTexts().getRight();
+            letCounter--;
+        }
+        
         if (!errorOccurred) {
             letD.getPremise().accept(this);
         }
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java
index ba23625..2857dde 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java
@@ -105,8 +105,6 @@ public class ExplanationCreatorUnification {
            if (isLetUnification) {
                createLetUnficiationFinish();
            }
-       } else if (isLetUnification) {
-           unificationTexts.remove(unificationTexts.size() - 1);
        }
    }
 
@@ -159,7 +157,6 @@ public class ExplanationCreatorUnification {
        return provider.getTranslation(textKey, locale);
    }
 
-   // WARNING: call toLatex() before to get proper latex code
    private String letCounterToLatex(String setName) {
        switch (letCounter) {
            case 0:
@@ -187,13 +184,8 @@ public class ExplanationCreatorUnification {
    }
 
    private void createUnficationTexts() {
-       List<UnificationStep> unificationSteps;
-       if (typeInferer.getUnificationSteps().isPresent()) {
-           unificationSteps = typeInferer.getUnificationSteps().get();
-       } else {
-           errorOccurred = true;
-           return;
-       }
+       List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
+               .orElseThrow(IllegalStateException::new);
 
        // skip first step since the substitutions list is still empty (unification introduction is shown)
        for (int stepNum = 1; stepNum < unificationSteps.size(); stepNum++) {
@@ -258,10 +250,8 @@ public class ExplanationCreatorUnification {
    private void createErrorText(UnificationError errorType) {
        if (errorType == UnificationError.INFINITE_TYPE) {
            unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "infiniteType"));
-           unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "infiniteType"));
        } else if (errorType == UnificationError.DIFFERENT_TYPES) {
            unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "differentTypes"));
-           unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "differentTypes"));
        }
    }