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 unificationSteps; - if (typeInferer.getUnificationSteps().isPresent()) { - unificationSteps = typeInferer.getUnificationSteps().get(); - } else { - errorOccurred = true; - return; - } + List 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")); } }