arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

highlight new constraints in unification

Browse Source
This commit is contained in:
Johanna Stuber 2021-03-10 19:38:51 +01:00
parent 5a1aaa8408
commit 47aa006655
2 changed files with 21 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java
View File

@ -54,7 +54,7 @@ public final class LatexCreatorConstants {
protected static final String CIRC = "\\circ"; protected static final String CIRC = "\\circ";
protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}"; protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}";
protected static final String COLOR_RED = "\\color{#f00}"; protected static final String COLOR_RED = "\\color{#f00}";
protected static final String COLOR_HIGHLIGHT = "\\color{#b0b}"; protected static final String COLOR_HIGHLIGHT = "\\color{#006AF5}";
protected static final String EMPTY_SET = "\\emptyset"; protected static final String EMPTY_SET = "\\emptyset";
protected static final String LAMBDA = "\\lambda"; protected static final String LAMBDA = "\\lambda";
protected static final String LATEX_SPACE = "\\ "; protected static final String LATEX_SPACE = "\\ ";

19
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
View File

@ -259,7 +259,8 @@ public class LatexCreatorConstraints implements StepVisitor {
.orElseThrow(IllegalStateException::new); .orElseThrow(IllegalStateException::new);
// store constraints of previous step to highlight changes // store constraints of previous step to highlight changes
String[] previousConstraints = new String[0]; String[] previousConstraints = new String[0];
for (UnificationStep step : unificationSteps) { for (int stepNum = 0; stepNum < unificationSteps.size(); stepNum++) {
UnificationStep step = unificationSteps.get(stepNum);
List<String> constraints2 = new ArrayList<>(); List<String> constraints2 = new ArrayList<>();
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions(); Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
Optional<UnificationError> error = Optional.empty(); Optional<UnificationError> error = Optional.empty();
@ -276,6 +277,9 @@ public class LatexCreatorConstraints implements StepVisitor {
boolean markError = error.isPresent(); boolean markError = error.isPresent();
List<Constraint> unificationConstraints = step.getConstraints(); List<Constraint> unificationConstraints = step.getConstraints();
// if new constraints were created in this step, mark them
boolean markLastTwoConstraints = (stepNum != 0)
&& unificationSteps.get(stepNum - 1).getConstraints().size() < unificationConstraints.size();
if (!unificationConstraints.isEmpty()) { if (!unificationConstraints.isEmpty()) {
latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT); latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT);
} }
@ -285,11 +289,14 @@ public class LatexCreatorConstraints implements StepVisitor {
if (markError && i == 0) { if (markError && i == 0) {
sb.append(CURLY_LEFT); sb.append(CURLY_LEFT);
sb.append(COLOR_RED); sb.append(COLOR_RED);
} else if (markLastTwoConstraints && (i < 2)) {
sb.append(CURLY_LEFT);
sb.append(COLOR_HIGHLIGHT);
} }
sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex()); sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex());
sb.append(EQUALS); sb.append(EQUALS);
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex()); sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex());
if (markError && i == 0) { if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) {
sb.append(CURLY_RIGHT); sb.append(CURLY_RIGHT);
} }
constraints2.add(sb.toString()); constraints2.add(sb.toString());
@ -299,13 +306,17 @@ public class LatexCreatorConstraints implements StepVisitor {
// perform the substitution "manually" and color the new type // perform the substitution "manually" and color the new type
Substitution s = substitutions.get(substitutions.size() - 1); Substitution s = substitutions.get(substitutions.size() - 1);
String original = previousConstraints[invIdx]; String original = previousConstraints[invIdx];
String originalType = new LatexCreatorType(s.getVariable()).getLatex();
if (original.contains(originalType)) {
StringBuilder highlightedChange2 = new StringBuilder(); StringBuilder highlightedChange2 = new StringBuilder();
highlightedChange2.append(CURLY_LEFT); highlightedChange2.append(CURLY_LEFT);
highlightedChange2.append(COLOR_HIGHLIGHT); highlightedChange2.append(COLOR_HIGHLIGHT);
highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex()); highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex());
highlightedChange2.append(CURLY_RIGHT); highlightedChange2.append(CURLY_RIGHT);
latex.append(original.replace(new LatexCreatorType(s.getVariable()).getLatex(), latex.append(original.replace(originalType, highlightedChange2.toString()));
highlightedChange2.toString())); } else {
latex.append(sb.toString());
}
} else { } else {
latex.append(sb.toString()); latex.append(sb.toString());
} }