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

Fix error coloring and translation

Browse Source
This commit is contained in:
Arne Keller 2021-02-12 15:26:48 +01:00
parent c46aee15a1
commit ecd92c9369
6 changed files with 39 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
frontend/src/mathjax-setup.js
View File

@ -4,7 +4,7 @@ SVGElement.prototype.getTransformToElement = SVGElement.prototype.getTransformTo
return elem.getScreenCTM().inverse().multiply(this.getScreenCTM());
};
window.MathJax = {
loader: {load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/colorv2', '[tex]/textmacros', '[tex]/unicode']},
loader: {load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/color', '[tex]/textmacros', '[tex]/unicode']},
tex: {
packages: {'[+]': ['ams', 'bussproofs', 'color', 'textmacros', 'unicode']},
inlineMath: [['$', '$'], ['\\(', '\\)']]

6
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java
View File

@ -14,6 +14,7 @@ import edu.kit.typicalc.view.content.ControlPanelView;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreator;
import java.util.List;
import java.util.Locale;
@PageTitle("TypeInferenceView")
@CssImport("./styles/view/type-inference.css")
@ -41,7 +42,10 @@ public class TypeInferenceView extends VerticalLayout
setId(ID);
setSizeFull();
addAttachListener(this);
lc = new LatexCreator(typeInferer);
// TODO: document new translation function
// TODO: is Function<UnificationError, String> too limiting?
lc = new LatexCreator(typeInferer,
error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)));
content = new Div();
content.setId(CONTENT_ID);
ControlPanel controlPanel = new ControlPanel(this, this);

17
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
View File

@ -2,12 +2,14 @@ package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.UnificationError;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.List;
import java.util.Map;
import java.util.function.Function;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
@ -28,22 +30,25 @@ public class LatexCreator implements StepVisitor {
* Generate the pieces of LaTeX-code from the type inferer.
*
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
* @param translationProvider translation text provider for {@link UnificationError}
*/
public LatexCreator(TypeInfererInterface typeInferer) {
this(typeInferer, true);
public LatexCreator(TypeInfererInterface typeInferer, Function<UnificationError, String> translationProvider) {
this(typeInferer, true, translationProvider);
}
/**
* Generate the pieces of LaTeX-code from the type inferer.
*
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
* @param stepLabels turns step labels on (true) or off (false)
* @param typeInferer theTypeInfererInterface to create the LaTeX code from
* @param stepLabels turns step labels on or off
* @param translationProvider translation text provider for {@link UnificationError}
*/
public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels) {
public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels,
Function<UnificationError, String> translationProvider) {
this.tree = new StringBuilder();
this.stepLabels = stepLabels;
typeInferer.getFirstInferenceStep().accept(this);
this.constraintsCreator = new LatexCreatorConstraints(typeInferer);
this.constraintsCreator = new LatexCreatorConstraints(typeInferer, translationProvider);
}
/**

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

@ -1,7 +1,9 @@
package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
/**
* Provides a list of constants needed for the creation of the LaTeX code.
* Provides a number of constants needed for the creation of LaTeX code in
* {@link LatexCreator}, {@link LatexCreatorConstraints}, {@link LatexCreatorTerm} and
* {@link LatexCreatorType}.
*/
public final class LatexCreatorConstants {
private LatexCreatorConstants() {
@ -47,7 +49,6 @@ public final class LatexCreatorConstants {
protected static final String LATEX_NEW_LINE = "\\\\";
protected static final String CIRC = "\\circ";
protected static final String PHANTOM_X = "\\phantom{x}";
protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}";
protected static final String COLOR_RED = "\\color{#f00}";
protected static final String LAMBDA = "\\lambda";

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

@ -7,6 +7,7 @@ import edu.kit.typicalc.util.Result;
import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
import java.util.function.Function;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
@ -25,27 +26,34 @@ public class LatexCreatorConstraints implements StepVisitor {
private final String constraintSetIndex;
private final String prefix;
private String prevStep;
private final Function<UnificationError, String> translationProvider;
/**
* Initializes the LatexCreatorConstraints with the right values calculates the strings
* that will be returned in getEverything().
*
* @param typeInferer the source for the generation of the LaTeX code
* @param translationProvider translation text provider for {@link UnificationError}
*/
protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
this(typeInferer, new ConstraintSetIndexFactory(), new TreeNumberGenerator(), FIRST_PREFIX);
protected LatexCreatorConstraints(TypeInfererInterface typeInferer,
Function<UnificationError, String> translationProvider) {
this(typeInferer,
new ConstraintSetIndexFactory(), new TreeNumberGenerator(),
FIRST_PREFIX, translationProvider);
}
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
ConstraintSetIndexFactory constraintSetIndexFactory,
TreeNumberGenerator numberGenerator,
String prefix) {
String prefix,
Function<UnificationError, String> translationProvider) {
this.prefix = prefix;
this.prevStep = "";
this.constraintSetIndexFactory = constraintSetIndexFactory;
this.numberGenerator = numberGenerator;
this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
this.typeInferer = typeInferer;
this.translationProvider = translationProvider;
constraints = new ArrayList<>();
if (FIRST_PREFIX.equals(prefix)) {
constraints.add(AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT);
@ -150,7 +158,8 @@ public class LatexCreatorConstraints implements StepVisitor {
addConstraint(letD);
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
constraintSetIndexFactory, numberGenerator,
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE,
translationProvider);
constraints.addAll(subCreator.getEverything());
// cancels constraint creation if sub inference failed
@ -218,8 +227,8 @@ public class LatexCreatorConstraints implements StepVisitor {
for (int i = unificationConstraints.size() - 1; i >= 0; i--) {
latex.append(AMPERSAND);
if (markError && i == 0) {
latex.append(COLOR_RED);
latex.append(CURLY_LEFT);
latex.append(COLOR_RED);
}
latex.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex());
latex.append(EQUALS);
@ -233,7 +242,6 @@ public class LatexCreatorConstraints implements StepVisitor {
}
}
if (!unificationConstraints.isEmpty()) {
// todo somehow this gets colored red too when an error occurs
latex.append(LATEX_CURLY_RIGHT + PAREN_RIGHT + LATEX_NEW_LINE);
}
@ -254,8 +262,8 @@ public class LatexCreatorConstraints implements StepVisitor {
latex.append(SPLIT_END);
if (error.isPresent()) {
latex.append(LATEX_NEW_LINE + AMPERSAND);
latex.append(translationProvider.apply(error.get()));
}
error.ifPresent(latex::append); // TODO: translation
steps.add(latex.toString());
}
return steps;

8
src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java
View File

@ -25,7 +25,7 @@ class LatexCreatorConstraintsTest {
@Test
void singleVarDefaultConstraintTest() {
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
List<String> actual = new LatexCreatorConstraints(typeInferer).getEverything();
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
String constraintSet = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS
+ GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT;
@ -55,7 +55,7 @@ class LatexCreatorConstraintsTest {
@Test
void singleAbsDefaultConstraintTest() {
typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap();
List<String> actual = new LatexCreatorConstraints(typeInferer).getEverything();
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
String constraintSet1 = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS
+ TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}" + LATEX_CURLY_RIGHT;
@ -102,7 +102,7 @@ class LatexCreatorConstraintsTest {
@Test
void singleAppConstraintTest() {
typeInferer = model.getTypeInferer("x y", new HashMap<>()).unwrap();
List<String> expected = new LatexCreatorConstraints(typeInferer).getEverything();
List<String> expected = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
List<String> actual = List.of(EMPTY_CONSTRAINT_SET,
ALIGN_BEGIN + AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{2}" + EQUALS
@ -118,7 +118,7 @@ class LatexCreatorConstraintsTest {
@Test
void singleConstConstraintTest() {
typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap();
List<String> expected = new LatexCreatorConstraints(typeInferer).getEverything();
List<String> expected = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
List<String> actual = List.of(EMPTY_CONSTRAINT_SET,
ALIGN_BEGIN + AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS