From 376933a4f549a2024fd9ce6c1be7dfd783088cd7 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 8 Oct 2021 11:51:53 +0200 Subject: [PATCH] Small code style fixes + documentation --- README.md | 3 +- frontend/styles/view/explanation.css | 3 -- frontend/styles/view/main/error-details.css | 3 -- frontend/styles/view/main/info-content.css | 4 --- .../{info-dialog.css => syntax-dialog.css} | 2 +- .../edu/kit/typicalc/model/ModelImpl.java | 6 ++-- .../edu/kit/typicalc/model/Unification.java | 4 +-- .../typicalc/model/parser/LambdaLexer.java | 2 +- .../typicalc/model/parser/LambdaParser.java | 10 +++--- .../java/edu/kit/typicalc/util/Result.java | 27 ++------------- .../java/edu/kit/typicalc/view/OVERVIEW.md | 12 ++++++- .../view/content/errorcontent/ErrorView.java | 8 ++--- .../MathjaxExplanation.java | 19 ++++++----- .../TypeInferenceView.java | 3 +- .../latexcreator/AssumptionGeneratorUtil.java | 18 +++++++++- .../latexcreator/LatexCreatorConstants.java | 5 +-- .../latexcreator/LatexCreatorConstraints.java | 34 ++++++++++++++++--- .../latexcreator/LatexCreatorMode.java | 7 ++++ .../latexcreator/LatexCreatorType.java | 2 -- .../latexcreator/TreeNumberGenerator.java | 4 +-- .../edu/kit/typicalc/view/main/InputBar.java | 2 +- .../{InfoContent.java => SyntaxContent.java} | 12 +++---- .../{InfoDialog.java => SyntaxDialog.java} | 10 +++--- .../view/main/TermExampleContent.java | 2 +- .../language/translation_de.properties | 3 +- .../language/translation_en.properties | 2 +- .../model/parser/LambdaParserTest.java | 4 --- 27 files changed, 115 insertions(+), 96 deletions(-) delete mode 100644 frontend/styles/view/explanation.css delete mode 100644 frontend/styles/view/main/error-details.css delete mode 100644 frontend/styles/view/main/info-content.css rename frontend/styles/view/main/{info-dialog.css => syntax-dialog.css} (92%) rename src/main/java/edu/kit/typicalc/view/main/{InfoContent.java => SyntaxContent.java} (82%) rename src/main/java/edu/kit/typicalc/view/main/{InfoDialog.java => SyntaxDialog.java} (85%) diff --git a/README.md b/README.md index 65c1eab..974387d 100644 --- a/README.md +++ b/README.md @@ -30,8 +30,7 @@ You can now also attach break points in code for debugging purposes, by clicking ### Running tests To run the unit tests and checkstyle: `mvn test`. -To run the integration tests: `mvn integration-test` (note that due to OS platform differences, it is unlikely that -you will get a 100% match on the first attempt.) +To run the integration tests: `mvn integration-test` (note that the screenshots are outdated, so the tests will fail..). ## Technical documentation Documentation on the application is contained in this file and the Javadocs in each source file. diff --git a/frontend/styles/view/explanation.css b/frontend/styles/view/explanation.css deleted file mode 100644 index 1e66f4a..0000000 --- a/frontend/styles/view/explanation.css +++ /dev/null @@ -1,3 +0,0 @@ -#tc-content { - overflow-y: auto; -} \ No newline at end of file diff --git a/frontend/styles/view/main/error-details.css b/frontend/styles/view/main/error-details.css deleted file mode 100644 index 52a2dbc..0000000 --- a/frontend/styles/view/main/error-details.css +++ /dev/null @@ -1,3 +0,0 @@ -[part="toggle"] { - color: white; -} \ No newline at end of file diff --git a/frontend/styles/view/main/info-content.css b/frontend/styles/view/main/info-content.css deleted file mode 100644 index 505c156..0000000 --- a/frontend/styles/view/main/info-content.css +++ /dev/null @@ -1,4 +0,0 @@ -#inputSyntax { - font-family: "Courier", serif; - margin-top: 1.5em; -} \ No newline at end of file diff --git a/frontend/styles/view/main/info-dialog.css b/frontend/styles/view/main/syntax-dialog.css similarity index 92% rename from frontend/styles/view/main/info-dialog.css rename to frontend/styles/view/main/syntax-dialog.css index 7735f14..72b0756 100644 --- a/frontend/styles/view/main/info-dialog.css +++ b/frontend/styles/view/main/syntax-dialog.css @@ -9,7 +9,7 @@ align-items: flex-start; } -#input-syntax { +.input-syntax { font-family: "Courier"; margin-top: 1.5em; } \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/model/ModelImpl.java b/src/main/java/edu/kit/typicalc/model/ModelImpl.java index acf1e21..351726e 100644 --- a/src/main/java/edu/kit/typicalc/model/ModelImpl.java +++ b/src/main/java/edu/kit/typicalc/model/ModelImpl.java @@ -32,18 +32,18 @@ public class ModelImpl implements Model { LambdaParser parser = new LambdaParser(lambdaTerm); Result result = parser.parse(); if (result.isError()) { - return new Result<>(null, result.unwrapError()); + return result.castError(); } //Parse Type Assumptions TypeAssumptionParser assumptionParser = new TypeAssumptionParser(); Result, ParseError> assumptionMap = assumptionParser.parse(typeAssumptions); if (assumptionMap.isError()) { - return new Result<>(null, assumptionMap.unwrapError()); + return assumptionMap.castError(); } // scope variables LambdaTerm term = result.unwrap(); term.accept(new ScopingVisitor()); TypeInferer typeInferer = new TypeInferer(term, assumptionMap.unwrap()); - return new Result<>(typeInferer, null); + return new Result<>(typeInferer); } } diff --git a/src/main/java/edu/kit/typicalc/model/Unification.java b/src/main/java/edu/kit/typicalc/model/Unification.java index d738458..4dee31c 100644 --- a/src/main/java/edu/kit/typicalc/model/Unification.java +++ b/src/main/java/edu/kit/typicalc/model/Unification.java @@ -33,8 +33,8 @@ public class Unification { Type b = c.getSecondType(); Result actions = a.constrainEqualTo(b); if (actions.isError()) { - steps.add(new UnificationStep(new Result<>(actions), new ArrayList<>(constraints), Optional.of(c))); - substitutionsResult = new Result<>(actions); + steps.add(new UnificationStep(actions.castError(), new ArrayList<>(constraints), Optional.of(c))); + substitutionsResult = actions.castError(); return; } UnificationActions thisStep = actions.unwrap(); diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java index 19bf9f6..e6d9431 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java @@ -35,7 +35,7 @@ public class LambdaLexer { while (true) { Result token = parseNextToken(); if (token.isError()) { - result = new Result<>(null, token.unwrapError()); + result = token.castError(); return; } Token value = token.unwrap(); diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java index ffb22d0..1d5cb41 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java @@ -158,7 +158,7 @@ public class LambdaParser { } Result varTerm = parseVar(); if (varTerm.isError()) { - return new Result<>(varTerm); + return varTerm.castError(); } error = expect(TokenType.EQUALS); if (error.isPresent()) { @@ -166,7 +166,7 @@ public class LambdaParser { } Result def = parseTerm(false); if (def.isError()) { - return new Result<>(def); + return def.castError(); } error = expect(TokenType.IN); if (error.isPresent()) { @@ -174,7 +174,7 @@ public class LambdaParser { } Result body = parseTerm(false); if (body.isError()) { - return new Result<>(body); + return body.castError(); } return new Result<>(new LetTerm(varTerm.unwrap(), def.unwrap(), body.unwrap())); } @@ -190,9 +190,9 @@ public class LambdaParser { Result varTerm = parseVar(); return new Result<>(varTerm.unwrap()); // variable token can always be parsed case LAMBDA: - return new Result<>(parseAbstraction()); + return parseAbstraction().castError(); case LET: - return new Result<>(parseLet()); + return parseLet().castError(); case TRUE: case FALSE: String boolText = token.getText(); diff --git a/src/main/java/edu/kit/typicalc/util/Result.java b/src/main/java/edu/kit/typicalc/util/Result.java index cc8aa6c..2fba46d 100644 --- a/src/main/java/edu/kit/typicalc/util/Result.java +++ b/src/main/java/edu/kit/typicalc/util/Result.java @@ -23,17 +23,6 @@ public class Result { this.error = null; } - /** - * Creates a new result by copying another one. - * - * @param other the result - */ - @SuppressWarnings("unchecked") - public Result(Result other) { - this.value = (T) other.value; - this.error = (E) other.error; - } - /** * Creates a new result containing the given value or error. * Only one of the parameters may be non-null. @@ -78,19 +67,6 @@ public class Result { return value; } - /** - * If the result contains a regular value, returns that value. - * Otherwise return the supplied alternative value. - * - * @return the value or the alternative - */ - public T unwrapOr(T alternative) { - if (value == null) { - return alternative; - } - return value; - } - /** * If the result contains an error, returns that error. * Otherwise an IllegalStateException is thrown. @@ -123,8 +99,9 @@ public class Result { * @param the desired type * @return a copy of this object */ + @SuppressWarnings("unchecked") public Result castError() { - return new Result<>(null, this.error); + return new Result<>((U) this.value, this.error); } @Override diff --git a/src/main/java/edu/kit/typicalc/view/OVERVIEW.md b/src/main/java/edu/kit/typicalc/view/OVERVIEW.md index fef758b..916078a 100644 --- a/src/main/java/edu/kit/typicalc/view/OVERVIEW.md +++ b/src/main/java/edu/kit/typicalc/view/OVERVIEW.md @@ -39,4 +39,14 @@ If a step label is targeted, a tooltip is rendered next to it (was very annoying The last paragraph requires that some elements of the proof tree / unification steps are marked using HTML classes and CSS IDs. It would be useless to expose this implementation detail to end users (especially since the relevant LaTeX macros are unlikely to be defined in the user's environment). -Note that the actual content is the same for both "modes". \ No newline at end of file +Note that the actual content is the same for both "modes". + +### Special character (∀, λ) input + +This is handled by a script (`input-bar-enhancements.ts`) in the user's browser, to reduce latency. +The buttons next to the input fields are also handled the same way. + +### Browser history + +Each click on the 'type' button results in a new history entry. Care has been taken that using the back/next buttons +in the browser actually works (see `UI.navigate` in `MainViewImpl.processInput`). \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/view/content/errorcontent/ErrorView.java b/src/main/java/edu/kit/typicalc/view/content/errorcontent/ErrorView.java index b771719..9639c92 100644 --- a/src/main/java/edu/kit/typicalc/view/content/errorcontent/ErrorView.java +++ b/src/main/java/edu/kit/typicalc/view/content/errorcontent/ErrorView.java @@ -14,7 +14,7 @@ import edu.kit.typicalc.model.parser.AdditionalInformation; import edu.kit.typicalc.model.parser.ExpectedInput; import edu.kit.typicalc.model.parser.ParseError; import edu.kit.typicalc.model.parser.Token; -import edu.kit.typicalc.view.main.InfoContent; +import edu.kit.typicalc.view.main.SyntaxContent; import java.util.Collection; import java.util.Optional; @@ -41,11 +41,11 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver { errorMessage = new Div(); container.add(heading, errorMessage); - InfoContent infoContent = new InfoContent(); + SyntaxContent syntaxContent = new SyntaxContent(); hint = new Paragraph(); - infoContent.addComponentAsFirst(hint); + syntaxContent.addComponentAsFirst(hint); - add(container, infoContent); + add(container, syntaxContent); } private String errorMessageForToken(Token token) { diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java index 75899d8..8dd51b6 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java @@ -3,7 +3,6 @@ package edu.kit.typicalc.view.content.typeinferencecontent; import com.vaadin.flow.component.ClientCallable; import com.vaadin.flow.component.Html; import com.vaadin.flow.component.Tag; -import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dependency.JsModule; import com.vaadin.flow.component.html.Div; import com.vaadin.flow.component.littemplate.LitTemplate; @@ -11,17 +10,17 @@ import com.vaadin.flow.component.template.Id; import edu.kit.typicalc.view.MathjaxAdapter; import java.util.List; +import java.util.function.Consumer; /** * Renders the constraints and unification (LaTeX, using MathJax) and allows step-by- - * step revealing. Relies on MathjaxUnificationTS to interact with MathJax. + * step revealing. */ @Tag("tc-explanation") @JsModule("./src/mathjax-explanation.ts") -@CssImport("./styles/view/explanation.css") public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter { - private final TypeInferenceView typeInferenceView; + private final transient Consumer stepSwitchCallback; private final List latex; // initialized by Vaadin @@ -31,15 +30,16 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter { /** * Creates a new HTML element that renders the provided texts. * - * @param view the type inference view this explanation text is attached to + * @param stepSwitchCallback the callback used when the user clicks on one of the texts * @param latex the latex texts for all steps * @param initialStep the step to show initially */ - public MathjaxExplanation(TypeInferenceView view, List latex, int initialStep) { - this.typeInferenceView = view; + public MathjaxExplanation(Consumer stepSwitchCallback, List latex, int initialStep) { + this.stepSwitchCallback = stepSwitchCallback; this.latex = latex; StringBuilder finalTex = new StringBuilder("
"); for (int i = 0; i < latex.size(); i++) { + // this class/id is used by the frontend script to locate texts finalTex.append(String.format("

", i)); finalTex.append(latex.get(i)); finalTex.append("

"); @@ -59,9 +59,12 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter { getElement().callJsFunction("showStep", n); } + /** + * Called when the user clicks on the explanation text of a specific step. + */ @ClientCallable private void switchToStep(int unificationStepIdx) { - typeInferenceView.setCurrentStep(unificationStepIdx); + stepSwitchCallback.accept(unificationStepIdx); } } 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 1fed82a..f35f458 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 @@ -130,7 +130,8 @@ public class TypeInferenceView extends VerticalLayout container.setId(CONTENT_ID2); unification = new MathjaxUnification(lc.getUnification()); var explainer = new ExplanationCreator(typeInferer, getLocale()); - this.explanation = new MathjaxExplanation(this, explainer.getExplanationTexts(), this.currentStep); + this.explanation = new MathjaxExplanation( + this::setCurrentStep, explainer.getExplanationTexts(), this.currentStep); if (tree == null) { tree = new MathjaxProofTree(lc.getTree(), stepAnnotations); 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 14e2d20..8f2d801 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,7 +18,15 @@ public final class AssumptionGeneratorUtil { private AssumptionGeneratorUtil() { } - protected static String typeAssumptionsToLatex(Map typeAssumptions, + /** + * Converts some type assumptions into LaTeX code to display them. + * Basic structure: name: Type, otherName: OtherType + * + * @param typeAssumptions the type assumptions + * @param mode latex creator mode + * @return the latex code + */ + static String typeAssumptionsToLatex(Map typeAssumptions, LatexCreatorMode mode) { if (typeAssumptions.isEmpty()) { return ""; @@ -37,6 +45,14 @@ public final class AssumptionGeneratorUtil { } } + /** + * Return the latex code for a given type abstraction, e.g.: + * ∀t1. t1 -> t1 + * + * @param abs the type abstraction + * @param mode latex creator mode + * @return the latex code + */ public static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) { StringBuilder abstraction = new StringBuilder(); if (abs.hasQuantifiedVariables()) { diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java index c7abf22..02c4202 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java @@ -43,8 +43,6 @@ public final class LatexCreatorConstants { protected static final char BRACKET_RIGHT = ']'; protected static final String LABEL_ABS = "\\LeftLabel{\\textrm A{\\small BS}}"; - protected static final String LABEL_ABS_WITH_CLASS = - "\\LeftLabel{\\class{typicalc-label typicalc-label-abs}{\\textrm A{\\small BS}}}"; protected static final String LABEL_APP = "\\LeftLabel{\\textrm A{\\small PP}}"; protected static final String LABEL_CONST = "\\LeftLabel{\\textrm C{\\small ONST}}"; protected static final String LABEL_VAR = "\\LeftLabel{\\textrm V{\\small AR}}"; @@ -73,7 +71,6 @@ public final class LatexCreatorConstants { protected static final String FOR_ALL = "\\forall"; protected static final String MONO_TEXT = "\\texttt"; protected static final String BOLD_TEXT = "\\textbf"; - protected static final String TEXT = "\\text"; protected static final String RIGHT_ARROW = "\\rightarrow"; protected static final String INSTANTIATE_SIGN = "\\succeq"; protected static final String LATEX_IN = "\\in"; @@ -86,7 +83,7 @@ public final class LatexCreatorConstants { protected static final String SPLIT_END = "\\end{split}"; /** - * Not actually a LaTeX command, but understood by MathJax. + * Not actually a LaTeX command, but understood by MathJax / the browser. */ protected static final String BREAK_ROW = "
"; } 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 2096ec9..4a4d06b 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 @@ -127,6 +127,14 @@ public class LatexCreatorConstraints implements StepVisitor { return numberGenerator.getNumbers(); } + /** + * Returns the latex code to display a single constraint: + * type1 = type2 + * + * @param constraint the constraint + * @param mode latex creator mode (if MathJax, adds the step index to the constraint) + * @return the latex code + */ public static String createSingleConstraint(Constraint constraint, LatexCreatorMode mode) { String firstType = new LatexCreatorType(constraint.getFirstType(), mode).getLatex(); String secondType = new LatexCreatorType(constraint.getSecondType(), mode).getLatex(); @@ -248,19 +256,28 @@ public class LatexCreatorConstraints implements StepVisitor { return latex; } + /** + * Main method of this class, creates the latex code for each step of the unification. + * + * @param constraintSets current constraint set (added to the latex) + * @return latex code for each step + */ private List generateUnification(String constraintSets) { List steps = new ArrayList<>(); List unificationSteps = typeInferer.getUnificationSteps() .orElseThrow(IllegalStateException::new); // store constraints of previous step to highlight changes - String[] previousConstraints = new String[0]; + List previousConstraints = new ArrayList<>(); + for (int stepNum = 0; stepNum < unificationSteps.size(); stepNum++) { UnificationStep step = unificationSteps.get(stepNum); List constraints2 = new ArrayList<>(); Result, UnificationError> subs = step.getSubstitutions(); Optional error = Optional.empty(); if (subs.isError()) { + // display previous step again + // and show the error message error = Optional.of(subs.unwrapError()); step = unificationSteps.get(unificationSteps.size() - 2); subs = step.getSubstitutions(); @@ -277,32 +294,37 @@ public class LatexCreatorConstraints implements StepVisitor { // if new constraints were created in this step, mark them boolean markLastTwoConstraints = (stepNum != 0) && unificationSteps.get(stepNum - 1).getConstraints().size() < unificationConstraints.size(); + + // render each constraint present in this step if (!unificationConstraints.isEmpty()) { latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT); } for (int i = unificationConstraints.size() - 1; i >= 0; i--) { latex.append(AMPERSAND); StringBuilder sb = new StringBuilder(); + boolean highligthingConstraint = false; if (markError && i == 0) { sb.append(CURLY_LEFT); sb.append(COLOR_RED); + highligthingConstraint = true; } else if (markLastTwoConstraints && (i < 2)) { sb.append(CURLY_LEFT); sb.append(COLOR_HIGHLIGHTED); + highligthingConstraint = true; } sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType(), mode).getLatex()); sb.append(EQUALS); sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType(), mode).getLatex()); - if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) { + if (highligthingConstraint) { sb.append(CURLY_RIGHT); } constraints2.add(sb.toString()); int invIdx = unificationConstraints.size() - 1 - i; // if this constraint was modified by the substitution - if (invIdx < previousConstraints.length) { + if (invIdx < previousConstraints.size()) { // perform the substitution "manually" and color the new type Substitution s = substitutions.get(substitutions.size() - 1); - String original = previousConstraints[invIdx]; + String original = previousConstraints.get(invIdx); String originalType = new LatexCreatorType(s.getVariable(), mode).getLatex(); if (original.contains(originalType)) { StringBuilder highlightedChange2 = new StringBuilder(); @@ -326,8 +348,9 @@ public class LatexCreatorConstraints implements StepVisitor { constraints2.remove(constraints2.size() - 1); latex.append(LATEX_CURLY_RIGHT + PAREN_RIGHT + LATEX_NEW_LINE); } - previousConstraints = constraints2.toArray(new String[0]); + previousConstraints = constraints2; + // also render the substitutions for (int i = substitutions.size() - 1; i >= 0; i--) { if (!unificationConstraints.isEmpty() || i != substitutions.size() - 1) { latex.append(CIRC); @@ -343,6 +366,7 @@ public class LatexCreatorConstraints implements StepVisitor { latex.delete(latex.length() - LATEX_NEW_LINE.length(), latex.length()); latex.append(SPLIT_END); latex.append(ALIGN_END + MATH_END); + // finally, display the error if there is one error.ifPresent(unificationError -> latex.append(translationProvider.apply(unificationError))); steps.add(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 index a31740e..97f3720 100644 --- 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 @@ -4,6 +4,13 @@ package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator; * Used to switch between different LaTeX generation methods. */ public enum LatexCreatorMode { + /** + * This mode adds a few HTML classes and ids to the generated LaTeX to facilitate highlighting etc. + * See OVERVIEW.md in the view package for more details. + */ MATHJAX, + /** + * Regular LaTeX mode. Doesn't use any MathJax extensions. + */ 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 26b53e3..8448da6 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 @@ -15,7 +15,6 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La * @see Type */ public class LatexCreatorType implements TypeVisitor { - private final Type type; private static final int MAX_LENGTH = 100000; // 100 KB private final LatexCreatorMode mode; @@ -28,7 +27,6 @@ public class LatexCreatorType implements TypeVisitor { * @param type the type */ public LatexCreatorType(Type type, LatexCreatorMode mode) { - this.type = type; this.mode = mode; type.accept(this); } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/TreeNumberGenerator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/TreeNumberGenerator.java index 5952cd4..b0eae68 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/TreeNumberGenerator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/TreeNumberGenerator.java @@ -20,7 +20,7 @@ public class TreeNumberGenerator { } /** - * Push the current index. Translates into the tree not doing anything in this step. + * Push the current index. This means that the tree will not change in this step. */ protected void push() { if (current < 0) { @@ -30,7 +30,7 @@ public class TreeNumberGenerator { } /** - * Push an incremented index. Translates into the tree going to the next step. + * Push an incremented index. This advances the proof tree. */ protected void incrementPush() { current++; diff --git a/src/main/java/edu/kit/typicalc/view/main/InputBar.java b/src/main/java/edu/kit/typicalc/view/main/InputBar.java index df2351d..3736ea9 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -139,7 +139,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { } private void onInfoIconClick() { - Dialog infoDialog = new InfoDialog(); + Dialog infoDialog = new SyntaxDialog(); infoDialog.open(); } diff --git a/src/main/java/edu/kit/typicalc/view/main/InfoContent.java b/src/main/java/edu/kit/typicalc/view/main/SyntaxContent.java similarity index 82% rename from src/main/java/edu/kit/typicalc/view/main/InfoContent.java rename to src/main/java/edu/kit/typicalc/view/main/SyntaxContent.java index 7127af8..f35eb8b 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InfoContent.java +++ b/src/main/java/edu/kit/typicalc/view/main/SyntaxContent.java @@ -9,10 +9,10 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; /** * Component which contains information on the correct syntax of the term as well as the type assumptions. */ -public class InfoContent extends VerticalLayout implements LocaleChangeObserver { +public class SyntaxContent extends VerticalLayout implements LocaleChangeObserver { private static final long serialVersionUID = 7193916603756938225L; - private static final String GRAMMAR_ID = "input-syntax"; + private static final String GRAMMAR_CLASS = "input-syntax"; private final Span termExplanation; private final Paragraph termSyntax; @@ -21,16 +21,16 @@ public class InfoContent extends VerticalLayout implements LocaleChangeObserver private final Paragraph typeSyntax; /** - * Creates a new InfoContent. + * Creates a new SyntaxContent. */ - public InfoContent() { + public SyntaxContent() { termExplanation = new Span(); termSyntax = new Paragraph(); assExplanation = new Span(); typeExplanation = new Span(); typeSyntax = new Paragraph(); - termSyntax.setId(GRAMMAR_ID); - typeSyntax.setId(GRAMMAR_ID); + termSyntax.setClassName(GRAMMAR_CLASS); + typeSyntax.setClassName(GRAMMAR_CLASS); add(termExplanation, termSyntax, assExplanation, typeExplanation, typeSyntax); } diff --git a/src/main/java/edu/kit/typicalc/view/main/InfoDialog.java b/src/main/java/edu/kit/typicalc/view/main/SyntaxDialog.java similarity index 85% rename from src/main/java/edu/kit/typicalc/view/main/InfoDialog.java rename to src/main/java/edu/kit/typicalc/view/main/SyntaxDialog.java index 768fd78..1c2eeea 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InfoDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/SyntaxDialog.java @@ -11,8 +11,8 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout; /** * Dialog which contains information on the correct syntax for the users input. */ -@CssImport("./styles/view/main/info-dialog.css") -public class InfoDialog extends Dialog { +@CssImport("./styles/view/main/syntax-dialog.css") +public class SyntaxDialog extends Dialog { private static final long serialVersionUID = 2914411566361539614L; /* @@ -23,9 +23,9 @@ public class InfoDialog extends Dialog { private static final String CLOSE_ICON_CLASS = "close-icon"; /** - * Creates new InfoDialog. + * Creates new SyntaxDialog. */ - protected InfoDialog() { + protected SyntaxDialog() { H4 heading = new H4(getTranslation("root.inputSyntax")); HorizontalLayout infoHeader = new HorizontalLayout(heading); Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL); @@ -34,7 +34,7 @@ public class InfoDialog extends Dialog { infoHeader.setId(INFO_HEADER_ID); infoHeader.add(closeIcon); - VerticalLayout infoContent = new InfoContent(); + VerticalLayout infoContent = new SyntaxContent(); infoContent.setId(INFO_CONTENT_ID); add(infoHeader, infoContent); diff --git a/src/main/java/edu/kit/typicalc/view/main/TermExampleContent.java b/src/main/java/edu/kit/typicalc/view/main/TermExampleContent.java index 924c5e2..7445418 100644 --- a/src/main/java/edu/kit/typicalc/view/main/TermExampleContent.java +++ b/src/main/java/edu/kit/typicalc/view/main/TermExampleContent.java @@ -8,7 +8,7 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout; /** * Contains all predefined examples as buttons. - * Clicking on a button selects the example and allows the user to chose between various type assumptions. + * Clicking on a button selects the example and allows the user to choose between various type assumptions. */ public class TermExampleContent extends VerticalLayout { private static final long serialVersionUID = 2882744650931562239L; diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index d1422e2..6c883fa 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -75,7 +75,8 @@ root.helpShortcuts=Strg + \u2190 = Erster Schritt
\ root.helpHoverEffects=Durch das Hovern über den Typherleitungsbaum und die Unifikation können zusätzliche Informationen \ angezeigt werden. Das Hovern über eine beliebige Variable im Typherleitungsbaum oder der Unifikation führt dazu, dass \ alle Vorkommen dieser Variable farblich hervorgehoben werden. Beim Hovern über die Schrift einer beliebigen Regel im \ -Typherleitungsbaum wird die Regel allgemein und die Instanziierung aller vorkommenden Variablen angezeigt. +Typherleitungsbaum wird die Regel allgemein und die Instanziierung aller vorkommenden Variablen angezeigt. \ +Außerdem wird der von diesem Schritt erzeugte Constraint hervorgehoben. root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funktion des Knopfs. \ Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Benutzen des Knopfs zurück zum ersten Schritt des \ Typherleitungsbaums. Wenn bereits die Unifikation durchgeführt wird, springt die Anzeige nach Benutzen des Knopfs \ diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties index 41c1f85..3f212f4 100644 --- a/src/main/resources/language/translation_en.properties +++ b/src/main/resources/language/translation_en.properties @@ -72,7 +72,7 @@ root.helpShortcuts=Ctrl + \u2190 = First step
\ root.helpHoverEffects=Additional information can be displayed by hovering over the inference tree and the unification. \ Hovering over an arbitrary variable in the tree or the unification highlights all occurences of this variable. Hovering \ over the label of an inference rule in the tree displays the general scheme of the rule as well as the instantiation of \ -all occuring variables. +all occuring variables. Additionally the constraint added in that step is highlighted in the unification area above. root.helpFirstStepButton=The function of the button depends on the current state of the algorithm. \ If the tree is currently being built up, clicking on the button shows the first step of the inference tree. \ If the unification algorithm is already in progress, clicking on the button shows the last step of the inference \ diff --git a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java index 415d05e..e9a44cf 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java @@ -65,10 +65,6 @@ class LambdaParserTest { void complicatedTerm() { LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)"); Result term = parser.parse(); - if (term.isError()) { - System.err.println(term.unwrapError()); - System.err.println(term.unwrapError().getCause()); - } assertEquals( new AppTerm( new AppTerm(