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 060be9a..7fc45d4 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 @@ -25,7 +25,7 @@ public final class AssumptionGeneratorUtil { } else { StringBuilder assumptions = new StringBuilder(); typeAssumptions.forEach(((varTerm, typeAbstraction) -> { - String termLatex = new LatexCreatorTerm(varTerm).getLatex(); + String termLatex = new LatexCreatorTerm(varTerm, mode).getLatex(); String abstraction = generateTypeAbstraction(typeAbstraction, mode); assumptions.append(termLatex) .append(COLON) 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 6bfede2..9923713 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 @@ -85,7 +85,7 @@ public class LatexCreator implements StepVisitor { private String conclusionToLatex(Conclusion conclusion) { String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode); - String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex(); + String term = new LatexCreatorTerm(conclusion.getLambdaTerm(), mode).getLatex(); String type = new LatexCreatorType(conclusion.getType()).getLatex(mode); return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN; } @@ -105,7 +105,7 @@ public class LatexCreator implements StepVisitor { private String generateVarStepPremise(VarStep var) { String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions(), mode); - String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex(); + String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm(), mode).getLatex(); String type = generateTypeAbstraction(var.getTypeAbsInPremise(), mode); return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term + PAREN_RIGHT + EQUALS + type; @@ -134,7 +134,7 @@ public class LatexCreator implements StepVisitor { @Override public void visit(ConstStepDefault constD) { tree.insert(0, generateConclusion(constD, LABEL_CONST, UIC)); - String visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm()).getLatex(); + String visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm(), mode).getLatex(); String step = AXC + CURLY_LEFT + DOLLAR_SIGN + visitorBuffer + SPACE + LATEX_IN + SPACE + CONST + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE; tree.insert(0, step); 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 c8af79c..d3e3b55 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 @@ -409,7 +409,7 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append(PAREN_LEFT); latex.append(typeAssumptions); latex.append("" + PAREN_RIGHT + COMMA + LATEX_SPACE); - latex.append(new LatexCreatorTerm(letVariable.orElseThrow(IllegalStateException::new)).getLatex()); + latex.append(new LatexCreatorTerm(letVariable.orElseThrow(IllegalStateException::new), mode).getLatex()); latex.append("" + COLON + TYPE_ABSTRACTION + PAREN_LEFT + SIGMA); latex.append(constraintSetIndex); latex.append(PAREN_LEFT); diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java index 3781e19..b943d54 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java @@ -11,8 +11,8 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La * @see LambdaTerm */ public class LatexCreatorTerm implements TermVisitor { - private final StringBuilder latex = new StringBuilder(); + private final LatexCreatorMode mode; private enum ParenthesesNeeded { NEVER, @@ -27,7 +27,8 @@ public class LatexCreatorTerm implements TermVisitor { * * @param lambdaTerm the term to convert into LaTeX */ - protected LatexCreatorTerm(LambdaTerm lambdaTerm) { + protected LatexCreatorTerm(LambdaTerm lambdaTerm, LatexCreatorMode mode) { + this.mode = mode; lambdaTerm.accept(this); } @@ -78,10 +79,18 @@ public class LatexCreatorTerm implements TermVisitor { @Override public void visit(VarTerm varTerm) { + if (mode == LatexCreatorMode.MATHJAX) { + latex.append("\\class{typicalc-type typicalc-type-v-"); + latex.append(varTerm.hashCode()); + latex.append("}{"); + } latex.append(MONO_TEXT); latex.append(CURLY_LEFT); latex.append(varTerm.getName()); latex.append(CURLY_RIGHT); + if (mode == LatexCreatorMode.MATHJAX) { + latex.append("}"); + } needsParentheses = ParenthesesNeeded.NEVER; } diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTermTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTermTest.java index 0b51f67..e8b33b4 100644 --- a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTermTest.java +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTermTest.java @@ -20,35 +20,40 @@ class LatexCreatorTermTest { typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap(); assertEquals(LAMBDA + SPACE + MONO_TEXT + "{x}" + DOT_SIGN + LATEX_SPACE + MONO_TEXT + "{y}", - new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex()); + new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), + LatexCreatorMode.NORMAL).getLatex()); } @Test void appTest() { typeInferer = model.getTypeInferer("x y", new HashMap<>()).unwrap(); assertEquals(MONO_TEXT + "{x}" + LATEX_SPACE + MONO_TEXT + "{y}", - new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex()); + new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), + LatexCreatorMode.NORMAL).getLatex()); } @Test void varTest() { typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap(); assertEquals(MONO_TEXT + "{x}", - new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex()); + new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), + LatexCreatorMode.NORMAL).getLatex()); } @Test void integerTest() { typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap(); assertEquals(MONO_TEXT + "{5}", - new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex()); + new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), + LatexCreatorMode.NORMAL).getLatex()); } @Test void booleanTest() { typeInferer = model.getTypeInferer("true", new HashMap<>()).unwrap(); assertEquals(MONO_TEXT + "{true}", - new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex()); + new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), + LatexCreatorMode.NORMAL).getLatex()); } @Test @@ -57,7 +62,8 @@ class LatexCreatorTermTest { assertEquals(MONO_TEXT + CURLY_LEFT + BOLD_TEXT + "{let}" + CURLY_RIGHT + LATEX_SPACE + MONO_TEXT + "{f}" + EQUALS + MONO_TEXT + "{x}" + LATEX_SPACE + MONO_TEXT + CURLY_LEFT + BOLD_TEXT + "{in}" + CURLY_RIGHT + LATEX_SPACE + MONO_TEXT + "{f}", - new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex()); + new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), + LatexCreatorMode.NORMAL).getLatex()); } @Test @@ -65,7 +71,8 @@ class LatexCreatorTermTest { typeInferer = model.getTypeInferer("x (y z)", new HashMap<>()).unwrap(); assertEquals(MONO_TEXT + "{x}" + LATEX_SPACE + PAREN_LEFT + MONO_TEXT + "{y}" + LATEX_SPACE + MONO_TEXT + "{z}" + PAREN_RIGHT, - new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex()); + new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), + LatexCreatorMode.NORMAL).getLatex()); } }