mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
Fixes exception thrown by last example
Not the most beautiful fix, but it works...
This commit is contained in:
parent
db48c7ffa0
commit
bbb0f7de38
@ -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<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
|
||||
.orElseThrow(IllegalStateException::new);
|
||||
List<UnificationStep> 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"));
|
||||
}
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user