arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-10 03:10:44 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
Moritz Dieing 2021-02-06 21:32:26 +01:00
commit d8b569c7b0
27 changed files with 154 additions and 99 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
frontend/src/mathjax-proof-tree.ts
View File

@ -27,10 +27,9 @@ class MathjaxProofTree extends MathjaxAdapter {
protected calculateSteps(): void {
if (this.shadowRoot !== null) {
const root = this.shadowRoot;
let semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
const semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
// first, enumerate all of the steps
let nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
let steps = [];
let a = null;
let stepIdx = 0;
while (a = nodeIterator.nextNode() as HTMLElement) {
@ -44,7 +43,7 @@ class MathjaxProofTree extends MathjaxAdapter {
stepIdx++;
}
}
// then fix some more mathjax layout issues
// then fix some mathjax layout issues
for (const step of root.querySelectorAll<HTMLElement>('g[typicalc="step"]')) {
const infRule = step.querySelector<HTMLElement>('g[semantics="bspr_inferenceRule:down"]');
if (infRule === null) {
@ -80,7 +79,7 @@ class MathjaxProofTree extends MathjaxAdapter {
}
// then create the steps
nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
steps = [];
let steps = [];
stepIdx = 0;
while (a = nodeIterator.nextNode() as HTMLElement) {
let semantics = a.getAttribute("semantics");
@ -92,12 +91,12 @@ class MathjaxProofTree extends MathjaxAdapter {
stepIdx++;
// find the next one/two steps above this one
const aboveStep1 = a.querySelector<HTMLElement>("#" + id + " g[typicalc=\"step\"]");
const aboveStep1 = a.querySelector<HTMLElement>("#" + id + ' g[typicalc="step"]');
let above = [];
if (aboveStep1 != null) {
const parent = aboveStep1.parentNode!.parentNode! as HTMLElement;
parent.setAttribute("id", "typicalc-selector");
for (const node of parent.querySelectorAll("#typicalc-selector > g > g[typicalc=\"step\"")) {
for (const node of parent.querySelectorAll('#typicalc-selector > g > g[typicalc="step"]')) {
above.push(node as HTMLElement);
}
parent.removeAttribute("id");
@ -123,17 +122,22 @@ class MathjaxProofTree extends MathjaxAdapter {
steps.push([a, above]);
}
}
// MathJax layout of bussproofs is sometimes wrong:
// https://github.com/mathjax/MathJax/issues/2270
// https://github.com/mathjax/MathJax/issues/2626
// the following algorithm fixes it by iterating over "rows" in the SVG created by MathJax
// in each row, the elements are arranged to not overlap
const svg = root.querySelector<SVGElement>("svg")!;
const nodeIterator2 = [...svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']")];
// start layout fixes in the innermost part of the SVG
nodeIterator2.reverse();
const padding = 300;
let counter = 0;
for (const a of nodeIterator2) {
for (const row of nodeIterator2) {
counter++;
let left = null;
let i = 0;
for (const rawNode of a.childNodes) {
for (const rawNode of row.childNodes) {
const node = rawNode as SVGGraphicsElement;
if (i === 1 || i === 3) {
i += 1;
@ -159,14 +163,13 @@ class MathjaxProofTree extends MathjaxAdapter {
}
parentNode = parentNode.childNodes[2] as SVGGraphicsElement;
const rule = node.querySelector<SVGGraphicsElement>('g [semantics="bspr_inferenceRule:down"]')!;
const term = rule.childNodes[1].childNodes[0].childNodes[0].childNodes[1].childNodes[0];
// this selector should be checked again when updating MathJax
const term = rule.childNodes[1].childNodes[0].childNodes[0].childNodes[1].childNodes[0] as SVGGraphicsElement;
// @ts-ignore
let w = -parentNode.getTransformToElement(term).e;
// @ts-ignore
w += term.getBBox().width;
w += padding;
// @ts-ignore
parentNode.setAttribute("x2", w);
parentNode.setAttribute("x2", w.toString());
}
i += 1;
}

11
frontend/src/mathjax-setup.js
View File

@ -144,10 +144,7 @@ mjx-container {\
}
}
};
(function () {
let script = document.createElement('script');
script.src = 'http://cdn.jsdelivr.net/npm/mathjax@3.1.2/es5/startup.js';
// script.async = true;
document.head.appendChild(script);
})();
// disable MathJax context menu
window.addEventListener("contextmenu", function (event) {
event.stopPropagation();
}, true);

1
frontend/src/tex-svg-full.js Normal file
View File

File diff suppressed because one or more lines are too long

16
frontend/styles/shared-styles.js
View File

@ -1,16 +0,0 @@
// eagerly import theme styles so as we can override them
import '@vaadin/vaadin-lumo-styles/all-imports';
const $_documentContainer = document.createElement('template');
$_documentContainer.innerHTML = `
<custom-style>
<style>
</style>
</custom-style>
`;
document.head.appendChild($_documentContainer.content);

5
src/main/java/edu/kit/typicalc/TypicalcConfiguration.java
View File

@ -7,12 +7,15 @@ import org.springframework.context.annotation.Bean;
import org.springframework.context.annotation.Configuration;
import org.springframework.web.servlet.config.annotation.WebMvcConfigurer;
/**
* This class configures some server properties related to HTTP.
*/
@Configuration
public class TypicalcConfiguration implements WebMvcConfigurer {
@Bean
public TomcatContextCustomizer sameSiteCookiesConfig() {
return context -> {
final Rfc6265CookieProcessor cookieProcessor = new Rfc6265CookieProcessor();
Rfc6265CookieProcessor cookieProcessor = new Rfc6265CookieProcessor();
cookieProcessor.setSameSiteCookies(SameSiteCookies.STRICT.getValue());
context.setCookieProcessor(cookieProcessor);
};

8
src/main/java/edu/kit/typicalc/model/TypeInfererLet.java
View File

@ -13,8 +13,8 @@ import java.util.Map;
import java.util.Optional;
/**
* Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps.
* They provide an extended constructor to make sure this sub-inference is consistent with the „outer“ inference.
* Instances of this implementation of TypeInfererInterface are used to execute the sub-inference starting in let steps.
* They provide an extended constructor to make sure this sub-inference is consistent with the "outer" inference.
*/
public class TypeInfererLet implements TypeInfererInterface {
@ -43,7 +43,7 @@ public class TypeInfererLet implements TypeInfererInterface {
unification = Optional.of(new Unification(new ArrayDeque<>(tree.getConstraints())));
// cancel algorithm if term can't be typified
// cancel algorithm if term can't be typed
if (unification.get().getSubstitutions().isError()) {
typeInfResult = Optional.empty();
return;
@ -59,7 +59,7 @@ public class TypeInfererLet implements TypeInfererInterface {
* C := { αi = σ(αi) | σ defined for αi }
*
* @return the constraints needed in the outer inference
* @throws IllegalStateException if the method is called despite missing mgu
* @throws IllegalStateException if the method is called despite missing MGU
*/
public List<Constraint> getLetConstraints() {
if (this.getMGU().isEmpty()) {

3
src/main/java/edu/kit/typicalc/model/Unification.java
View File

@ -31,6 +31,7 @@ public class Unification {
steps.add(new UnificationStep(new Result<>(Collections.emptyList()), new ArrayList<>(constraints)));
while (!constraints.isEmpty()) {
Constraint c = constraints.removeFirst();
// calculate the result of this constraint
Type a = c.getFirstType();
Type b = c.getSecondType();
Result<UnificationActions, UnificationError> actions = a.constrainEqualTo(b);
@ -41,6 +42,7 @@ public class Unification {
}
UnificationActions thisStep = actions.unwrap();
Optional<Substitution> substitution = thisStep.getSubstitution();
// apply substitution to remaining constraints
if (substitution.isPresent()) {
Deque<Constraint> updateConstraints = new ArrayDeque<>();
for (Constraint constraint : constraints) {
@ -54,6 +56,7 @@ public class Unification {
constraints = updateConstraints;
substitutions.add(substitution.get());
}
// add new constraints to the queue
constraints.addAll(thisStep.getConstraints());
steps.add(new UnificationStep(new Result<>(new ArrayList<>(substitutions)), new ArrayList<>(constraints)));
}

15
src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java
View File

@ -14,7 +14,12 @@ import java.util.EnumSet;
import java.util.Optional;
import java.util.Set;
public class LambdaParser {
/**
* Parser for lambda terms.
*
* @see LambdaTerm
*/
public class LambdaParser { // TODO: document syntax above ^ ?
/**
* lexer to translate a String into tokens
*/
@ -33,6 +38,7 @@ public class LambdaParser {
/**
* Constructs a parser with the specified String
*
* @param term String to parse
*/
public LambdaParser(String term) {
@ -55,6 +61,7 @@ public class LambdaParser {
* Checks that the token type of current token matches the token type given as parameter.
* If successful, returns that token and advances to the next token.
* Returns false otherwise.
*
* @param type the token type to compare the current token type to
*/
private Optional<ParseError> expect(TokenType type) {
@ -69,7 +76,8 @@ public class LambdaParser {
/**
* Parses the String given in the constructor as a term.
* @return the term given by the String
*
* @return the term, or an error
*/
public Result<LambdaTerm, ParseError> parse() {
Result<LambdaTerm, ParseError> t = parseTerm(true);
@ -85,6 +93,7 @@ public class LambdaParser {
/**
* Parses a term.
*
* @return the term, or an error
*/
private Result<LambdaTerm, ParseError> parseTerm(boolean next) {
@ -135,6 +144,7 @@ public class LambdaParser {
/**
* Parses an application or constructs of higher precedence.
*
* @return the term, or an error
*/
private Result<LambdaTerm, ParseError> parseApplication() {
@ -187,6 +197,7 @@ public class LambdaParser {
/**
* Parses an atom (variable or number) or a parenthesised expression.
*
* @return the term
*/
private Result<LambdaTerm, ParseError> parseAtom() {

12
src/main/java/edu/kit/typicalc/model/parser/ParseError.java
View File

@ -1,5 +1,11 @@
package edu.kit.typicalc.model.parser;
/**
* Errors that can occur when parsing a lambda term.
*
* @see LambdaLexer
* @see LambdaParser
*/
public enum ParseError {
/**
@ -19,6 +25,12 @@ public enum ParseError {
private Token cause = new Token(Token.TokenType.EOF, "", -1);
/**
* Attach a token to this error.
*
* @param cause the token that caused the error
* @return this object
*/
public ParseError withToken(Token cause) {
this.cause = cause;
return this;

2
src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java
View File

@ -35,7 +35,7 @@ public class TypicalcI18NProvider implements I18NProvider {
@Override
public String getTranslation(String key, Locale locale, Object... params) {
final ResourceBundle bundle = ResourceBundle.getBundle(LANGUAGE_BUNDLE_PREFIX, locale);
ResourceBundle bundle = ResourceBundle.getBundle(LANGUAGE_BUNDLE_PREFIX, locale);
String translation;

1
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
View File

@ -1,6 +1,5 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.step.*;

17
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorTerm.java
View File

@ -4,17 +4,30 @@ import edu.kit.typicalc.model.term.*;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
/**
* Generates LaTeX code for lambda terms.
*
* @see LatexCreator
* @see LambdaTerm
*/
public class LatexCreatorTerm implements TermVisitor {
// TODO: document
private final StringBuilder latex;
private final StringBuilder latex = new StringBuilder();
private boolean needsParentheses = false;
/**
* Initialize a new latex creator object with a lambda term.
*
* @param lambdaTerm the term to convert into LaTeX
*/
protected LatexCreatorTerm(LambdaTerm lambdaTerm) {
this.latex = new StringBuilder();
lambdaTerm.accept(this);
}
/**
* @return the generated LaTeX code
*/
public String getLatex() {
// remove most outer parentheses if they exist
// if (latex.indexOf(PAREN_LEFT) == 0 && latex.indexOf(PAREN_RIGHT) == latex.length() - 1) {

11
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorType.java
View File

@ -8,10 +8,21 @@ import edu.kit.typicalc.model.type.TypeVisitor;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
/**
* Generates LaTeX code for types.
*
* @see LatexCreator
* @see Type
*/
public class LatexCreatorType implements TypeVisitor {
private final StringBuilder latex = new StringBuilder();
private boolean needsParentheses = false;
/**
* Initialize a new latex creator with a type.
*
* @param type the type
*/
protected LatexCreatorType(Type type) {
type.accept(this);
}

4
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java
View File

@ -10,8 +10,8 @@ import com.vaadin.flow.component.template.Id;
import edu.kit.typicalc.view.MathjaxAdapter;
/**
* Renders a tree from LaTeX using MathJax and allows for step-by-step-revealing for
* proof trees that use the bussproofs package. Relies on MathjaxProofTreeJS to interact
* Renders a tree from LaTeX using MathJax and allows step-by-step revealing of
* proof trees that use the bussproofs package. Relies on MathjaxProofTreeTS to interact
* with MathJax.
*/
@Tag("tc-proof-tree")

4
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java
View File

@ -9,8 +9,8 @@ import com.vaadin.flow.component.template.Id;
import edu.kit.typicalc.view.MathjaxAdapter;
/**
* Renders the constraints and unification from LaTeX using MathJax and allows step-by-
* step-revealing capabilities. Relies on MathjaxUnificationJS to interact with MathJax.
* Renders the constraints and unification (LaTeX, using MathJax) and allows step-by-
* step revealing. Relies on MathjaxUnificationTS to interact with MathJax.
*/
@Tag("tc-unification")
@JsModule("./src/mathjax-adapter.ts")

3
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java
View File

@ -7,13 +7,10 @@ import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.orderedlayout.Scroller;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.router.PageTitle;
import com.vaadin.flow.router.Route;
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.main.MainViewImpl;
@Route(value = "visualize", layout = MainViewImpl.class)
@PageTitle("TypeInferenceView")
@CssImport("./styles/view/type-inference.css")
public class TypeInferenceView extends VerticalLayout

6
src/main/java/edu/kit/typicalc/view/main/DrawerContent.java
View File

@ -24,14 +24,16 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
private final VerticalLayout ruleContainer;
/**
* Creates a new DrawerContent.
* Creates a new DrawerContent.
*/
protected DrawerContent() {
heading = new H3(getTranslation("root.inferenceRules"));
heading = new H3();
ruleContainer = new VerticalLayout();
ruleContainer.setId(RULE_CONTAINER_ID);
add(heading, ruleContainer);
setId(DRAWER_CONTENT_ID);
localeChange(null);
}
@Override

6
src/main/java/edu/kit/typicalc/view/main/ErrorNotification.java
View File

@ -14,9 +14,9 @@ public class ErrorNotification extends Notification {
private static final String NOTIFICATION_ID = "errorNotification";
protected ErrorNotification(String errorMessage) {
final VerticalLayout container = new VerticalLayout();
final Span errorSpan = new Span(errorMessage);
final Button closeButton = new Button(getTranslation("root.close"), event -> this.close());
VerticalLayout container = new VerticalLayout();
Span errorSpan = new Span(errorMessage);
Button closeButton = new Button(getTranslation("root.close"), event -> this.close());
container.add(errorSpan, closeButton);
container.setAlignItems(FlexComponent.Alignment.CENTER);

15
src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
View File

@ -11,8 +11,8 @@ import java.util.List;
import java.util.function.Consumer;
/**
* Contains all predefined examples as buttons. Clicking on a button inserts the example string into
* the input bar.
* Contains all predefined examples as buttons.
* Clicking on a button inserts the example string into the input field.
*
*/
public class ExampleDialog extends Dialog implements LocaleChangeObserver {
@ -27,14 +27,13 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
private final Paragraph instruction;
/**
* Creates a new ExampleDialog with a callback method to insert the example string into the input
* bar.
* Creates a new ExampleDialog with a callback method that will receive the selected example.
*
* @param callback inserts the string of the chosen example into the input bar
* @param callback function to handle the selected lambda term
*/
protected ExampleDialog(Consumer<String> callback) {
VerticalLayout layout = new VerticalLayout();
instruction = new Paragraph(getTranslation("root.selectExample"));
instruction = new Paragraph();
layout.add(instruction);
for (String term : EXAMPLES) {
Button button = new Button(term);
@ -42,11 +41,13 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
callback.accept(term);
this.close();
});
button.setId(term); // needed for IT
button.setId(term); // needed for integration test
layout.add(button);
}
add(layout);
setId(EXAMPLE_DIALOG_ID);
localeChange(null); // initialize text content
}
@Override

13
src/main/java/edu/kit/typicalc/view/main/HelpDialog.java
View File

@ -37,26 +37,27 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
* Create a new HelpDialog.
*/
protected HelpDialog() {
final HorizontalLayout headingLayout = new HorizontalLayout();
HorizontalLayout headingLayout = new HorizontalLayout();
renderer = item -> getTranslation("root." + item.getDisplayLanguage(Locale.ENGLISH).toLowerCase());
heading = new H3(getTranslation("root.operatingHelp"));
heading = new H3();
headingLayout.setId(HEADING_LAYOUT_ID);
languageSelect = new Select<>(Locale.GERMAN, Locale.ENGLISH);
languageSelect.setTextRenderer(renderer);
languageSelect.setLabel(getTranslation("root.selectLanguage"));
languageSelect.setValue(UI.getCurrent().getLocale());
languageSelect.addValueChangeListener(event -> UI.getCurrent().setLocale(event.getValue()));
languageSelect.setId(LANGUAGE_SELECT_ID);
headingLayout.add(heading, languageSelect);
final VerticalLayout contentLayout = new VerticalLayout();
VerticalLayout contentLayout = new VerticalLayout();
//TODO inputSyntax wird im inputDialog behandelt --> hier anderer Content
inputSyntax = new H5(getTranslation("root.inputSyntax"));
inputSyntax = new H5();
contentLayout.setId(CONTENT_LAYOUT_ID);
contentLayout.add(inputSyntax);
add(headingLayout, contentLayout);
localeChange(null);
}
@Override
public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.operatingHelp"));

4
src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java
View File

@ -45,13 +45,13 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
protected InferenceRuleField(String latex, String nameKey) {
this.nameKey = nameKey;
final HorizontalLayout header = new HorizontalLayout();
HorizontalLayout header = new HorizontalLayout();
header.setId(HEADER_ID);
this.ruleName = new H4(getTranslation(nameKey));
ruleName.setId(RULE_NAME_ID);
header.add(ruleName);
final VerticalLayout main = new VerticalLayout();
VerticalLayout main = new VerticalLayout();
main.setId(MAIN_ID);
this.copyButton = new Button(getTranslation("root.copyLatex"), new Icon(VaadinIcon.CLIPBOARD));
MathjaxDisplay rule = new MathjaxDisplay(latex); //TODO scale, when method implemented

12
src/main/java/edu/kit/typicalc/view/main/InfoDialog.java
View File

@ -25,26 +25,24 @@ public class InfoDialog extends Dialog {
private static final String GRAMMAR_ID = "inputSyntax";
private static final String CLOSE_ICON_ID = "closeIcon";
private final H4 heading;
/**
* Creates new InfoDialog.
*/
protected InfoDialog() {
heading = new H4(getTranslation("root.inputSyntax"));
H4 heading = new H4(getTranslation("root.inputSyntax"));
HorizontalLayout infoHeader = new HorizontalLayout(heading);
Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL);
closeIcon.addClickListener(event -> this.close());
closeIcon.setId(CLOSE_ICON_ID);
infoHeader.setId(INFO_HEADER_ID);
infoHeader.add(closeIcon);
VerticalLayout infoContent = createInfoContent();
infoContent.setId(INFO_CONTENT_ID);
add(infoHeader, infoContent);
}
private VerticalLayout createInfoContent() {
Span termExplanation = new Span(getTranslation("root.termExplanation"));
Paragraph termSyntax = new Paragraph();
@ -58,4 +56,6 @@ public class InfoDialog extends Dialog {
assSyntax.setId(GRAMMAR_ID);
return new VerticalLayout(termExplanation, termSyntax, assExplanation, assSyntax);
}
// local change observer is not needed, the dialog is created when it is opened
}

22
src/main/java/edu/kit/typicalc/view/main/InputBar.java
View File

@ -56,8 +56,24 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
inputField = new TextField();
inputField.setId(INPUT_FIELD_ID);
inputField.setClearButtonVisible(true);
inputField.setValueChangeMode(ValueChangeMode.EAGER);
inputField.addValueChangeListener(event -> onInputFieldValueChange());
inputField.setMaxLength(1000); // TODO: perhaps remove the error message? more than 1000 can't be entered now
inputField.setValueChangeMode(ValueChangeMode.EAGER); // TODO: this causes a lot of network traffic
inputField.addValueChangeListener(event -> onInputFieldValueChange());
// attach a listener that replaces \ with λ
// JavaScript is used because Vaadin does not have APIs for selectionStart/selectionEnd
/*
UI.getCurrent().getPage().executeJs(
"document.getElementById('" + INPUT_FIELD_ID + "').addEventListener('keyup', e => {"
+ "var area = e.target.shadowRoot.querySelector('input');"
+ "if (area.value.indexOf('\\\\') >= 0) {"
+ " var start = area.selectionStart;"
+ " var end = area.selectionEnd;"
+ " var textBefore = area.value.substr(0, end);"
+ " area.value = area.value.replace('\\\\', 'λ');"
+ " area.selectionStart = start;"
+ " area.selectionEnd = end;"
+ "}});");
*/
Button lambdaButton = new Button(getTranslation("root.lambda"), event -> onLambdaButtonClick());
typeAssumptions = new Button(
getTranslation("root.typeAssumptions"),
@ -105,7 +121,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
UI.getCurrent().getPage().setTitle(getTranslation("root.typicalc") + " - " + currentInput);
callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions()));
} else {
final Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput"));
Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput"));
errorNotification.open();
}
}

25
src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java
View File

@ -4,7 +4,6 @@ import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.applayout.AppLayout;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dependency.JavaScript;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.notification.Notification;
import com.vaadin.flow.router.*;
import edu.kit.typicalc.model.ModelImpl;
@ -27,10 +26,12 @@ import java.util.List;
*/
@CssImport("./styles/view/main/main-view.css")
@CssImport(value = "./styles/view/main/app-layout.css", themeFor = "vaadin-app-layout")
@JsModule("./styles/shared-styles.js")
@JavaScript("./src/svg-pan-zoom.min.js")
@JavaScript("./src/tex-svg-full.js")
@PageTitle("Typicalc")
public class MainViewImpl extends AppLayout implements MainView, HasErrorParameter<NotFoundException> {
@Route(TypeInferenceView.ROUTE + "/:term")
public class MainViewImpl extends AppLayout
implements MainView, BeforeEnterObserver, HasErrorParameter<NotFoundException> {
private static final long serialVersionUID = -2411433187835906976L;
private final UpperBar upperBar;
@ -55,15 +56,12 @@ public class MainViewImpl extends AppLayout implements MainView, HasErrorParamet
@Override
public void displayError(ParseError error) {
//TODO add error keys to bundle
final Notification errorNotification = new ErrorNotification(getTranslation("root." + error.toString()));
Notification errorNotification = new ErrorNotification(getTranslation("root." + error.toString()));
errorNotification.open();
}
@Override
public int setErrorParameter(
BeforeEnterEvent event,
ErrorParameter<NotFoundException> parameter) {
public void beforeEnter(BeforeEnterEvent event) {
if (event.getLocation().getPath().matches(TypeInferenceView.ROUTE + "/.*")) {
List<String> segments = event.getLocation().getSegments();
String term = segments.get(segments.size() - 1);
@ -73,11 +71,7 @@ public class MainViewImpl extends AppLayout implements MainView, HasErrorParamet
upperBar.inferTerm(StringUtils.EMPTY);
} else if (event.getLocation().getPath().equals(StringUtils.EMPTY)) {
setContent(new StartPageView());
} else {
setContent(new NotFoundView());
return HttpServletResponse.SC_NOT_FOUND;
}
return HttpServletResponse.SC_OK;
}
@ -89,4 +83,11 @@ public class MainViewImpl extends AppLayout implements MainView, HasErrorParamet
private String decodeURL(String encodedUrl) {
return java.net.URLDecoder.decode(encodedUrl, StandardCharsets.UTF_8);
}
@Override
public int setErrorParameter(BeforeEnterEvent event, ErrorParameter<NotFoundException> parameter) {
setContent(new NotFoundView());
// TODO: actually return a real 404 response (not 200)
return HttpServletResponse.SC_NOT_FOUND;
}
}

4
src/main/java/edu/kit/typicalc/view/main/MathjaxDisplay.java
View File

@ -8,8 +8,8 @@ import com.vaadin.flow.component.template.Id;
import edu.kit.typicalc.view.MathjaxAdapter;
/**
* Renders static LaTeX content using MathJax. Relies on MathjaxDisplayJS to interact
* with MathJax.
* Renders static LaTeX content using MathJax.
* Relies on MathjaxDisplayTS to interact with MathJax.
*/
@Tag("tc-display")
@JsModule("./src/mathjax-adapter.ts")

5
src/main/java/edu/kit/typicalc/view/main/NotFoundView.java
View File

@ -5,10 +5,11 @@ import com.vaadin.flow.component.html.H2;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.router.ParentLayout;
/**
* This is the view used when an unknown URL is requested by the user.
*/
@ParentLayout(MainViewImpl.class)
public class NotFoundView extends VerticalLayout {
public NotFoundView() {
H1 error404 = new H1("404 - Not found");
H2 suggestion = new H2("Try \"/infer/<term>\" or type your favourite term into the input field");

1
src/main/java/edu/kit/typicalc/view/main/UpperBar.java
View File

@ -65,7 +65,6 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
helpIcon.addClickListener(event -> onHelpIconClick());
helpIcon.setId(HELP_ICON_ID);
this.rules = new DrawerToggle();
rules.setText(getTranslation("root.inferenceRules"));
add(rules, viewTitle, inputBar, helpIcon);
setId(UPPER_BAR_ID);