From 61288712230b3a0377e3760ca9c3f9e7a8ef0b25 Mon Sep 17 00:00:00 2001 From: ucrhh Date: Fri, 12 Feb 2021 13:49:08 +0100 Subject: [PATCH] fix some todos --- .../latexcreator/LatexCreator.java | 18 +++++++++--------- .../latexcreator/LatexCreatorConstraints.java | 7 ------- 2 files changed, 9 insertions(+), 16 deletions(-) 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 fae5b72..ba6bdaa 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 @@ -69,11 +69,11 @@ public class LatexCreator implements StepVisitor { /** * Returns needed LaTeX packages * - * @return the packages needed for the LaTeX-code from getTree() and getUnification() to work + * @return the packages needed for the LaTeX-code from getTree() to work */ public String getLatexPackages() { return BUSSPROOFS; - } // todo implement + } @@ -120,8 +120,8 @@ public class LatexCreator implements StepVisitor { String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions()); String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex(); String type = generateTypeAbstraction(var.getTypeAbsInPremise()); - return DOLLAR_SIGN + PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term - + PAREN_RIGHT + EQUALS + type + DOLLAR_SIGN; + return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term + + PAREN_RIGHT + EQUALS + type; } private String generateTypeAbstraction(TypeAbstraction abs) { @@ -171,7 +171,8 @@ public class LatexCreator implements StepVisitor { @Override public void visit(VarStepDefault varD) { tree.insert(0, generateConclusion(varD, LABEL_VAR, UIC)); - tree.insert(0, AXC + CURLY_LEFT + generateVarStepPremise(varD) + CURLY_RIGHT + NEW_LINE); + tree.insert(0, AXC + CURLY_LEFT + DOLLAR_SIGN + generateVarStepPremise(varD) + + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE); } @Override @@ -182,9 +183,9 @@ public class LatexCreator implements StepVisitor { String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType + DOLLAR_SIGN + NEW_LINE; String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN - + generateVarStepPremise(varL).replace(DOLLAR_SIGN, "") - + SPACE + LATEX_NEW_LINE + SPACE // TODO: less replacement fixups - + premiseRight.replace(DOLLAR_SIGN, "") + + generateVarStepPremise(varL) + + SPACE + LATEX_NEW_LINE + SPACE + + premiseRight + ALIGN_END + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE; tree.insert(0, premiseLeft); } @@ -194,7 +195,6 @@ public class LatexCreator implements StepVisitor { tree.insert(0, generateConclusion(letD, LABEL_LET, BIC)); letD.getPremise().accept(this); letD.getTypeInferer().getFirstInferenceStep().accept(this); - // todo correct? } @Override 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 bd3e966..c89310a 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 @@ -200,14 +200,7 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append(CURLY_LEFT); } latex.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex()); - if (markError && i == 0) { - latex.append(CURLY_RIGHT); - } latex.append(EQUALS); - if (markError && i == 0) { - latex.append(COLOR_RED); - latex.append(CURLY_LEFT); - } latex.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex()); if (markError && i == 0) { latex.append(CURLY_RIGHT);