From 648b5f6752b630375252a6b2c4ba3e7107bae9f2 Mon Sep 17 00:00:00 2001
From: ucrhh <ucrhh@student.kit.edu>
Date: Sat, 6 Feb 2021 11:20:26 +0100
Subject: [PATCH] some doc and codestyle

---
 .../typeinferencecontent/LatexCreator.java    | 24 +++++++++++++++----
 1 file changed, 19 insertions(+), 5 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
index 83120da..4ee6c55 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
@@ -41,6 +41,12 @@ public class LatexCreator implements StepVisitor {
         this(typeInferer, true);
     }
 
+    /**
+     * 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)
+     */
     protected LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels) {
         this.typeInferer = typeInferer;
         this.tree = new StringBuilder();
@@ -50,6 +56,8 @@ public class LatexCreator implements StepVisitor {
     }
 
     /**
+     * Returns the proof tree
+     *
      * @return the LaTeX-code for the proof tree
      */
     protected String getTree() {
@@ -57,22 +65,29 @@ public class LatexCreator implements StepVisitor {
     }
 
     /**
+     * Returns the LaTeX-code for constraints, unification, MGU and MGU
+     *
      * @return the LaTeX-code for constraints and unification
      */
     protected String[] getUnification() {
         List<String> result = new ArrayList<>(constraintsGenerator.getConstraints());
         result.addAll(generateUnification());
         typeInferer.getMGU().ifPresent(mgu -> result.add(generateMGU()));
+        // todo return final type
         return result.toArray(new String[0]);
     } // todo implement
 
     /**
-     * @return the packages needed for the LaTeX-code from getTree() and getUnification()to work
+     * Returns needed LaTeX packages
+     *
+     * @return the packages needed for the LaTeX-code from getTree() and getUnification() to work
      */
     protected String getLatexPackages() {
         return BUSSPROOFS;
     } // todo implement
 
+
+
     private String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions) {
         //todo sort entries?
         if (typeAssumptions.isEmpty()) {
@@ -197,7 +212,6 @@ public class LatexCreator implements StepVisitor {
     }
 
 
-    // todo use generateConstraint
     @Override
     public void visit(AbsStepDefault absD) {
         tree.insert(0, generateConclusion(absD, LABEL_ABS, UIC));
@@ -239,11 +253,11 @@ public class LatexCreator implements StepVisitor {
         String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
         String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType
                 + DOLLAR_SIGN + NEW_LINE;
-        String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + "\\begin{align}"
+        String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
                 + generateVarStepPremise(varL).replace(DOLLAR_SIGN, "")
-                + " \\\\ " // TODO: less magic strings, less replacement fixups
+                + SPACE + LATEX_NEW_LINE + SPACE // TODO: less replacement fixups
                 + premiseRight.replace(DOLLAR_SIGN, "")
-                + "\\end{align}" + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
+                + ALIGN_END + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
         tree.insert(0, premiseLeft);
     }