Improve display of unification errors

This commit is contained in:
Arne Keller 2021-08-29 15:43:02 +02:00
parent 6bae4a3b01
commit 520960fea1
3 changed files with 5 additions and 11 deletions

View File

@ -342,12 +342,8 @@ public class LatexCreatorConstraints implements StepVisitor {
} }
latex.delete(latex.length() - LATEX_NEW_LINE.length(), latex.length()); latex.delete(latex.length() - LATEX_NEW_LINE.length(), latex.length());
latex.append(SPLIT_END); latex.append(SPLIT_END);
if (error.isPresent()) {
latex.append(LATEX_NEW_LINE + LATEX_NEW_LINE + AMPERSAND + TEXT + CURLY_LEFT);
latex.append(translationProvider.apply(error.get()));
latex.append(CURLY_RIGHT);
}
latex.append(ALIGN_END + MATH_END); latex.append(ALIGN_END + MATH_END);
error.ifPresent(unificationError -> latex.append(translationProvider.apply(unificationError)));
steps.add(latex.toString()); steps.add(latex.toString());
} }
return steps; return steps;

View File

@ -186,9 +186,9 @@ root.absLetLatex=\
\\end{prooftree} \\end{prooftree}
root.infinite_type = Der eingegebene Term ist nicht typisierbar: \ root.infinite_type = Der eingegebene Term ist nicht typisierbar: \
Durch den {\\color{#f00}hervorgehobenen} Constraint würde sich ein unendlicher Typ ergeben! Durch den hervorgehobenen} Constraint würde sich ein unendlicher Typ ergeben!
root.different_types = Der eingegebene Term ist nicht typisierbar: \ root.different_types = Der eingegebene Term ist nicht typisierbar: \
In dem {\\color{#f00}hervorgehobenen} Constraint werden zwei unvereinbare Typen gleichgesetzt! In dem hervorgehobenen Constraint werden zwei unvereinbare Typen gleichgesetzt!
share.heading=Teilen share.heading=Teilen
share.url.label=URL share.url.label=URL

View File

@ -174,10 +174,8 @@ root.absLetLatex=\
\\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\ \\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
\\end{prooftree} \\end{prooftree}
root.infinite_type = The entered term cannot be typed: \ root.infinite_type = The entered term cannot be typed: The highlighted constraint would cause an infinite type!
The {\\color{#f00}highlighted} constraint would cause an infinite type! root.different_types = The entered term cannot be typed: The highlighted constraint contains two incompatible types!
root.different_types = The entered term cannot be typed: \
The {\\color{#f00}highlighted} constraint contains two incompatible types!
share.heading=Share share.heading=Share
share.url.label=URL share.url.label=URL