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 4c36d85..7875ffa 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 @@ -85,6 +85,8 @@ public class ExplanationCreatorUnification { if (isLetUnification) { createLetUnficiationFinish(); } + } else if (isLetUnification) { + unificationTexts.remove(unificationTexts.size() - 1); } } @@ -165,8 +167,13 @@ public class ExplanationCreatorUnification { } private void createUnficationTexts() { - List unificationSteps = typeInferer.getUnificationSteps() - .orElseThrow(IllegalStateException::new); + List unificationSteps; + if (typeInferer.getUnificationSteps().isPresent()) { + unificationSteps = typeInferer.getUnificationSteps().get(); + } else { + errorOccurred = true; + return; + } // skip first step since the substitutions list is still empty (unification introduction is shown) for (int stepNum = 1; stepNum < unificationSteps.size(); stepNum++) { @@ -231,8 +238,10 @@ 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")); } }