From 74c21773d4c927e46f32adaea6e8dc9673e41283 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 21 Jun 2021 11:12:02 +0200 Subject: [PATCH] Only use hover classes when using Mathjax --- .../TypeInferenceView.java | 12 +++-- .../latexcreator/AssumptionGeneratorUtil.java | 11 ++-- .../latexcreator/LatexCreator.java | 26 ++++++---- .../latexcreator/LatexCreatorConstraints.java | 50 +++++++++++-------- .../latexcreator/LatexCreatorMode.java | 9 ++++ .../latexcreator/LatexCreatorType.java | 10 ++-- .../LatexCreatorConstraintsTest.java | 12 ++--- .../latexcreator/LatexCreatorTest.java | 4 +- .../latexcreator/LatexCreatorTypeTest.java | 10 ++-- .../resources/checkstyle-suppressions.xml | 3 ++ 10 files changed, 93 insertions(+), 54 deletions(-) create mode 100644 src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorMode.java diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index e1235a5..89edb23 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java @@ -20,6 +20,7 @@ import edu.kit.typicalc.model.TypeInfererInterface; import edu.kit.typicalc.view.content.ControlPanel; import edu.kit.typicalc.view.content.ControlPanelView; import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreator; +import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode; import edu.kit.typicalc.view.main.TypeInferenceRules; import edu.kit.typicalc.view.main.MainViewImpl; @@ -62,6 +63,7 @@ public class TypeInferenceView extends VerticalLayout private MathjaxUnification unification; private MathjaxProofTree tree = null; private transient LatexCreator lc; + private transient LatexCreator lcUser; private final transient TypeInfererInterface typeInferer; private final Div content; private final ControlPanel controlPanel; @@ -136,8 +138,8 @@ public class TypeInferenceView extends VerticalLayout UI.getCurrent().getPage().executeJs("return decodeURI(window.location.href)").then(url -> new ShareDialog( url.asString().replace(" ", "%20"), - lc.getTree(), - lc.getUnification()[currentStep]).open() + lcUser.getTree(), + lcUser.getUnification()[currentStep]).open() ); } @@ -197,7 +199,11 @@ public class TypeInferenceView extends VerticalLayout if (typeInferer != null) { content.removeAll(); lc = new LatexCreator(typeInferer, - error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH))); + error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)), + LatexCreatorMode.MATHJAX); + lcUser = new LatexCreator(typeInferer, + error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)), + LatexCreatorMode.NORMAL); treeNumbers = lc.getTreeNumbers(); setContent(); refreshElements(); diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java index 4bd3a4e..060be9a 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java @@ -18,14 +18,15 @@ public final class AssumptionGeneratorUtil { private AssumptionGeneratorUtil() { } - protected static String typeAssumptionsToLatex(Map typeAssumptions) { + protected static String typeAssumptionsToLatex(Map typeAssumptions, + LatexCreatorMode mode) { if (typeAssumptions.isEmpty()) { return ""; } else { StringBuilder assumptions = new StringBuilder(); typeAssumptions.forEach(((varTerm, typeAbstraction) -> { String termLatex = new LatexCreatorTerm(varTerm).getLatex(); - String abstraction = generateTypeAbstraction(typeAbstraction); + String abstraction = generateTypeAbstraction(typeAbstraction, mode); assumptions.append(termLatex) .append(COLON) .append(abstraction) @@ -36,18 +37,18 @@ public final class AssumptionGeneratorUtil { } } - protected static String generateTypeAbstraction(TypeAbstraction abs) { + protected static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) { StringBuilder abstraction = new StringBuilder(); if (abs.hasQuantifiedVariables()) { abstraction.append(FOR_ALL); abs.getQuantifiedVariables().forEach(typeVariable -> { - String variableTex = new LatexCreatorType(typeVariable).getLatex(); + String variableTex = new LatexCreatorType(typeVariable).getLatex(mode); abstraction.append(variableTex).append(COMMA); }); abstraction.deleteCharAt(abstraction.length() - 1); abstraction.append(DOT_SIGN); } - abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex()); + abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex(mode)); return abstraction.toString(); } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java index baf705f..6bfede2 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java @@ -22,6 +22,7 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La */ public class LatexCreator implements StepVisitor { private final StringBuilder tree; + private final LatexCreatorMode mode; private final boolean stepLabels; private final LatexCreatorConstraints constraintsCreator; @@ -30,9 +31,11 @@ public class LatexCreator implements StepVisitor { * * @param typeInferer theTypeInfererInterface to create the LaTeX-code from * @param translationProvider translation text provider for {@link UnificationError} + * @param mode LaTeX creation mode */ - public LatexCreator(TypeInfererInterface typeInferer, Function translationProvider) { - this(typeInferer, true, translationProvider); + public LatexCreator(TypeInfererInterface typeInferer, Function translationProvider, + LatexCreatorMode mode) { + this(typeInferer, true, translationProvider, mode); } /** @@ -41,13 +44,16 @@ public class LatexCreator implements StepVisitor { * @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} + * @param mode LaTeX creation mode */ public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels, - Function translationProvider) { + Function translationProvider, + LatexCreatorMode mode) { this.tree = new StringBuilder(); + this.mode = mode; this.stepLabels = stepLabels; typeInferer.getFirstInferenceStep().accept(this); - this.constraintsCreator = new LatexCreatorConstraints(typeInferer, translationProvider); + this.constraintsCreator = new LatexCreatorConstraints(typeInferer, translationProvider, mode); } /** @@ -78,9 +84,9 @@ public class LatexCreator implements StepVisitor { } private String conclusionToLatex(Conclusion conclusion) { - String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions()); + String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode); String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex(); - String type = new LatexCreatorType(conclusion.getType()).getLatex(); + String type = new LatexCreatorType(conclusion.getType()).getLatex(mode); return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN; } @@ -98,9 +104,9 @@ public class LatexCreator implements StepVisitor { } private String generateVarStepPremise(VarStep var) { - String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions()); + String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions(), mode); String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex(); - String type = generateTypeAbstraction(var.getTypeAbsInPremise()); + String type = generateTypeAbstraction(var.getTypeAbsInPremise(), mode); return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term + PAREN_RIGHT + EQUALS + type; } @@ -144,8 +150,8 @@ public class LatexCreator implements StepVisitor { @Override public void visit(VarStepWithLet varL) { tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC)); - String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise()); - String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex(); + String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise(), mode); + String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex(mode); String premiseRight = typeAbstraction + INSTANTIATE_SIGN + instantiatedType; String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN + generateVarStepPremise(varL) diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java index 0c1763c..c8af79c 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java @@ -37,6 +37,7 @@ public class LatexCreatorConstraints implements StepVisitor { private String prevStep; private final Function translationProvider; private int constraintsInCurrLine; + private final LatexCreatorMode mode; /** * Initializes the LatexCreatorConstraints with the right values calculates the strings @@ -46,10 +47,11 @@ public class LatexCreatorConstraints implements StepVisitor { * @param translationProvider translation text provider for {@link UnificationError} */ protected LatexCreatorConstraints(TypeInfererInterface typeInferer, - Function translationProvider) { + Function translationProvider, + LatexCreatorMode mode) { this(typeInferer, new ConstraintSetIndexFactory(), new TreeNumberGenerator(), - FIRST_PREFIX, Optional.empty(), Optional.empty(), translationProvider); + FIRST_PREFIX, Optional.empty(), Optional.empty(), translationProvider, mode); } private LatexCreatorConstraints(TypeInfererInterface typeInferer, @@ -58,7 +60,8 @@ public class LatexCreatorConstraints implements StepVisitor { String prefix, Optional letVariable, Optional> newTypeAssumption, - Function translationProvider) { + Function translationProvider, + LatexCreatorMode mode) { this.prefix = prefix; this.letVariable = letVariable; this.newTypeAssumption = newTypeAssumption; @@ -74,6 +77,7 @@ public class LatexCreatorConstraints implements StepVisitor { constraints.add(AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT); numberGenerator.incrementPush(); } + this.mode = mode; typeInferer.getFirstInferenceStep().accept(this); } @@ -129,8 +133,8 @@ public class LatexCreatorConstraints implements StepVisitor { } private String createSingleConstraint(Constraint constraint) { - String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex(); - String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex(); + String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex(mode); + String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex(mode); return firstType + EQUALS + secondType; } @@ -197,7 +201,7 @@ public class LatexCreatorConstraints implements StepVisitor { LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(), constraintSetIndexFactory, numberGenerator, constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE, Optional.of(term.getVariable()), - newTypeAss, translationProvider); + newTypeAss, translationProvider, mode); constraints.addAll(subCreator.getEverything()); // cancels constraint creation if sub inference failed @@ -293,9 +297,9 @@ public class LatexCreatorConstraints implements StepVisitor { sb.append(CURLY_LEFT); sb.append(COLOR_HIGHLIGHTED); } - sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex()); + sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex(mode)); sb.append(EQUALS); - sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex()); + sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex(mode)); if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) { sb.append(CURLY_RIGHT); } @@ -306,19 +310,19 @@ public class LatexCreatorConstraints implements StepVisitor { // perform the substitution "manually" and color the new type Substitution s = substitutions.get(substitutions.size() - 1); String original = previousConstraints[invIdx]; - String originalType = new LatexCreatorType(s.getVariable()).getLatex(); + String originalType = new LatexCreatorType(s.getVariable()).getLatex(mode); if (original.contains(originalType)) { StringBuilder highlightedChange2 = new StringBuilder(); highlightedChange2.append(CURLY_LEFT); highlightedChange2.append(COLOR_HIGHLIGHTED); - highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex()); + highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex(mode)); highlightedChange2.append(CURLY_RIGHT); latex.append(original.replace(originalType, highlightedChange2.toString())); } else { - latex.append(sb.toString()); + latex.append(sb); } } else { - latex.append(sb.toString()); + latex.append(sb); } if (i > 0) { latex.append(COMMA); @@ -337,9 +341,9 @@ public class LatexCreatorConstraints implements StepVisitor { } latex.append(BRACKET_LEFT); latex.append(AMPERSAND); - latex.append(new LatexCreatorType(substitutions.get(i).getVariable()).getLatex()); + latex.append(new LatexCreatorType(substitutions.get(i).getVariable()).getLatex(mode)); latex.append(SUBSTITUTION_SIGN); - latex.append(new LatexCreatorType(substitutions.get(i).getType()).getLatex()); + latex.append(new LatexCreatorType(substitutions.get(i).getType()).getLatex(mode)); latex.append(BRACKET_RIGHT); latex.append(LATEX_NEW_LINE); } @@ -364,9 +368,9 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append(BRACKET_LEFT); typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> { latex.append(AMPERSAND); - latex.append(new LatexCreatorType(substitution.getVariable()).getLatex()); + latex.append(new LatexCreatorType(substitution.getVariable()).getLatex(mode)); latex.append(SUBSTITUTION_SIGN); - latex.append(new LatexCreatorType(substitution.getType()).getLatex()); + latex.append(new LatexCreatorType(substitution.getType()).getLatex(mode)); latex.append(COMMA); latex.append(LATEX_NEW_LINE); })); @@ -382,16 +386,18 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append(SIGMA); latex.append(constraintSetIndex); latex.append(PAREN_LEFT); - latex.append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex()); + latex.append( + new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode)); latex.append("" + PAREN_RIGHT + EQUALS); - latex.append(new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new)).getLatex()); + latex.append( + new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new)).getLatex(mode)); return latex.toString(); } // generates the TypeAssumptions for the right sub tree of a let step private String generateNewTypeAssumptions(String subPrefix) { InferenceStep step = typeInferer.getFirstInferenceStep(); - String typeAssumptions = typeAssumptionsToLatex(step.getConclusion().getTypeAssumptions()); + String typeAssumptions = typeAssumptionsToLatex(step.getConclusion().getTypeAssumptions(), mode); if ("".equals(typeAssumptions)) { typeAssumptions = EMPTY_SET; } @@ -407,13 +413,15 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append("" + COLON + TYPE_ABSTRACTION + PAREN_LEFT + SIGMA); latex.append(constraintSetIndex); latex.append(PAREN_LEFT); - latex.append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex()); + latex.append( + new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode) + ); latex.append("" + PAREN_RIGHT + COMMA + SIGMA); latex.append(constraintSetIndex); latex.append(PAREN_LEFT); latex.append(typeAssumptions); latex.append("" + PAREN_RIGHT + PAREN_RIGHT + EQUALS); - latex.append(typeAssumptionsToLatex(newTypeAssumption.orElseThrow(IllegalSelectorException::new))); + latex.append(typeAssumptionsToLatex(newTypeAssumption.orElseThrow(IllegalSelectorException::new), mode)); return latex.toString(); } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorMode.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorMode.java new file mode 100644 index 0000000..a31740e --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorMode.java @@ -0,0 +1,9 @@ +package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator; + +/** + * Used to switch between different LaTeX generation methods. + */ +public enum LatexCreatorMode { + MATHJAX, + NORMAL +} diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java index 1b2ab27..26883af 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java @@ -34,9 +34,13 @@ public class LatexCreatorType implements TypeVisitor { /** * @return the generated LaTeX code */ - protected String getLatex() { - // this class is used in frontend/src/mathjax-setup.js - return "\\class{typicalc-type typicalc-type-" + type.hashCode() + "}{" + latex + "}"; + protected String getLatex(LatexCreatorMode mode) { + if (mode == LatexCreatorMode.MATHJAX) { + // this class is used in frontend/src/mathjax-setup.js + return "\\class{typicalc-type typicalc-type-" + type.hashCode() + "}{" + latex + "}"; + } else { + return latex.toString(); + } } @Override diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java index c3740d9..3fc0fcd 100644 --- a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java @@ -26,7 +26,7 @@ class LatexCreatorConstraintsTest { @Test void singleVarDefaultConstraintTest() { typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap(); - List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything(); String constraintSet = AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + AMPERSAND + TREE_VARIABLE + "_{1}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT @@ -56,7 +56,7 @@ class LatexCreatorConstraintsTest { @Test void singleAbsDefaultConstraintTest() { typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap(); - List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything(); String constraintSet1 = AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + AMPERSAND + TREE_VARIABLE + "_{1}" + EQUALS + TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE @@ -104,12 +104,12 @@ class LatexCreatorConstraintsTest { @Test void lineBreak() { typeInferer = model.getTypeInferer("a b c d e f", new HashMap<>()).unwrap(); - List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything(); assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{2}=\\alpha_{3} \\rightarrow \\alpha_{1},\\alpha_{4}=\\alpha_{5} \\rightarrow \\alpha_{2},\\alpha_{6}=\\alpha_{7} \\rightarrow \\alpha_{4},\\alpha_{8}=\\alpha_{9} \\rightarrow \\alpha_{6},\\alpha_{10}=\\alpha_{11} \\rightarrow \\alpha_{8},\\alpha_{10}=\\beta_{1},\\alpha_{11}=\\beta_{2},\\alpha_{9}=\\beta_{3},\\alpha_{7}=\\beta_{4},\\alpha_{5}=\\beta_{5},\\\\&\\alpha_{3}=\\beta_{6}\\}\\end{split}\\end{aligned}", actual.get(11)); typeInferer = model.getTypeInferer("let g = a b c d e f in g", new HashMap<>()).unwrap(); - actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything(); assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{1}=\\alpha_{13}\\}\\end{split}\\\\\n" + "&\\begin{split}C_{let}=\\{&\\alpha_{3}=\\alpha_{4} \\rightarrow \\alpha_{2},\\alpha_{5}=\\alpha_{6} \\rightarrow \\alpha_{3},\\alpha_{7}=\\alpha_{8} \\rightarrow \\alpha_{5},\\alpha_{9}=\\alpha_{10} \\rightarrow \\alpha_{7},\\alpha_{11}=\\alpha_{12} \\rightarrow \\alpha_{9},\\alpha_{11}=\\beta_{1},\\alpha_{12}=\\beta_{2},\\alpha_{10}=\\beta_{3},\\alpha_{8}=\\beta_{4},\\alpha_{6}=\\beta_{5},\\\\&\\alpha_{4}=\\beta_{6}\\}\\end{split}\\end{aligned}", actual.get(12)); @@ -118,7 +118,7 @@ class LatexCreatorConstraintsTest { @Test void emptyLetTypeAssumptions() { typeInferer = model.getTypeInferer("let g = 5 in g", new HashMap<>()).unwrap(); - List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything(); assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{1}=\\alpha_{3}\\}\\end{split}\\\\\n" + "&\\begin{split}C_{let}=\\{&\\alpha_{2}=\\texttt{int}\\}\\end{split}\\\\&\\begin{split}\\sigma_{let}:=\\textit{mgu}(C_{let})=[&\\alpha_{2}\\mathrel{\\unicode{x21E8}}\\texttt{int}]\\end{split}\\\\&\\sigma_{let}(\\alpha_{2})=\\texttt{int}\\\\&\\Gamma'=\\sigma_{let}(\\emptyset),\\ \\texttt{g}:ta(\\sigma_{let}(\\alpha_{2}),\\sigma_{let}(\\emptyset))=\\texttt{g}:\\texttt{int}\\end{aligned}", actual.get(6)); } @@ -127,7 +127,7 @@ class LatexCreatorConstraintsTest { void excessiveMemoryUsageAvoided() { try { typeInferer = model.getTypeInferer("(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)", new HashMap<>()).unwrap(); - List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything(); // should have thrown IllegalStateException by now fail("did not throw exception"); } catch (IllegalStateException e) { diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTest.java index 9497cde..c1a7f8b 100644 --- a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTest.java +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTest.java @@ -15,7 +15,7 @@ class LatexCreatorTest { @Test void testFailedLet() { TypeInfererInterface typeInferer = model.getTypeInferer("let fun = 5 5 in fun 42", new HashMap<>()).unwrap(); - String latex = new LatexCreator(typeInferer, Enum::toString).getTree(); + String latex = new LatexCreator(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getTree(); assertEquals("\\begin{prooftree}\n" + "\\AxiomC{$\\texttt{5} \\in Const$}\n" + "\\LeftLabel{\\textrm C{\\small ONST}}\n" + @@ -30,7 +30,7 @@ class LatexCreatorTest { "\\BinaryInfC{$\\vdash\\texttt{\\textbf{let}}\\ \\texttt{fun}=\\texttt{5}\\ \\texttt{5}\\ \\texttt{\\textbf{in}}\\ \\texttt{fun}\\ \\texttt{42}:\\alpha_{1}$}\n" + "\\end{prooftree}", latex); typeInferer = model.getTypeInferer("(let fun = 5 5 in fun) 42", new HashMap<>()).unwrap(); - latex = new LatexCreator(typeInferer, Enum::toString).getTree(); + latex = new LatexCreator(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getTree(); assertEquals("\\begin{prooftree}\n" + "\\AxiomC{$\\texttt{5} \\in Const$}\n" + "\\LeftLabel{\\textrm C{\\small ONST}}\n" + diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java index 498816b..a5acbc9 100644 --- a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java @@ -19,20 +19,21 @@ class LatexCreatorTypeTest { void identityTest() { typeInferer = model.getTypeInferer("λx.x", new HashMap<>()).unwrap(); assertEquals(TREE_VARIABLE + "_{2} " + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{2}", - new LatexCreatorType(typeInferer.getType().get()).getLatex()); + new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); } @Test void generatedTypeTest() { typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap(); assertEquals(GENERATED_ASSUMPTION_VARIABLE + "_{1}", - new LatexCreatorType(typeInferer.getType().get()).getLatex()); + new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); } @Test void namedTypeTest() { typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap(); - assertEquals(MONO_TEXT + "{int}", new LatexCreatorType(typeInferer.getType().get()).getLatex()); + assertEquals(MONO_TEXT + "{int}", + new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); } @Test @@ -40,6 +41,7 @@ class LatexCreatorTypeTest { HashMap map = new HashMap<>(); map.put("x", "t1"); typeInferer = model.getTypeInferer("x", map).unwrap(); - assertEquals(USER_VARIABLE + "_{1}", new LatexCreatorType(typeInferer.getType().get()).getLatex()); + assertEquals(USER_VARIABLE + "_{1}", + new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); } } diff --git a/src/test/resources/checkstyle-suppressions.xml b/src/test/resources/checkstyle-suppressions.xml index 0aff2fd..c33eaf0 100644 --- a/src/test/resources/checkstyle-suppressions.xml +++ b/src/test/resources/checkstyle-suppressions.xml @@ -6,5 +6,8 @@ +