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

DRY translation setup + Vaadin bug workaround

Browse Source
This commit is contained in:
Arne Keller 2021-02-11 12:27:10 +01:00
parent a00cd12d2e
commit 7878b5fc83
10 changed files with 79 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/main/java/edu/kit/typicalc/Application.java
View File

@ -2,11 +2,16 @@ package edu.kit.typicalc;
import com.vaadin.flow.component.page.AppShellConfigurator;
import com.vaadin.flow.server.ServiceInitEvent;
import com.vaadin.flow.server.VaadinServiceInitListener;
import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
import org.springframework.boot.SpringApplication;
import org.springframework.boot.autoconfigure.SpringBootApplication;
import org.springframework.boot.web.servlet.support.SpringBootServletInitializer;
import org.vaadin.artur.helpers.LaunchUtil;
import java.util.regex.Pattern;
/**
* The entry point of the Spring Boot application.
*
@ -14,10 +19,25 @@ import org.vaadin.artur.helpers.LaunchUtil;
*
*/
@SpringBootApplication
public class Application extends SpringBootServletInitializer implements AppShellConfigurator {
public class Application extends SpringBootServletInitializer
implements AppShellConfigurator, VaadinServiceInitListener {
private static final Pattern ROUTE_PATTERN = Pattern.compile("/" + TypeInferenceView.ROUTE + "/[^/]+");
public static void main(String[] args) {
LaunchUtil.launchBrowserInDevelopmentMode(SpringApplication.run(Application.class, args));
}
@Override
public void serviceInit(ServiceInitEvent event) {
event.addRequestHandler((session, request, response) -> {
// Vaadin does not set the error code:
// https://github.com/vaadin/flow/issues/8942
String url = request.getPathInfo();
if (!url.equals("/") && !ROUTE_PATTERN.matcher(url).matches()) {
response.setHeader("X-ME", "test");
response.setStatus(404);
}
return false;
});
}
}

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

@ -12,14 +12,12 @@ import java.util.Map;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
/**
* Generates LaTeX-code from a TypeInfererInterface object. Two mostly independent pie-
* ces of code are generated, one for the constraints/unification and one for the proof tree.
* The LaTeX-code is created in a form, that it can be rendered by MathJax, so it must
* only use packages and commands that MathJax supports. The LaTeX code is also usable
* outside of MathJax, in a normal .tex document.
* Generates LaTeX code from a TypeInfererInterface object. Two mostly independent pieces
* of code are generated: one for the constraints/unification and one for the proof tree.
* The LaTeX code can be rendered by MathJax, so it must only use packages and commands that MathJax supports.
* The LaTeX code is also usable outside of MathJax, in a normal LaTeX document.
*/
public class LatexCreator implements StepVisitor {
private final TypeInfererInterface typeInferer;
private final StringBuilder tree;
private final boolean stepLabels;
private final LatexCreatorConstraints constraintsCreator;
@ -40,7 +38,6 @@ public class LatexCreator implements StepVisitor {
* @param stepLabels turns step labels on (true) or off (false)
*/
public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels) {
this.typeInferer = typeInferer;
this.tree = new StringBuilder();
this.stepLabels = stepLabels;
typeInferer.getFirstInferenceStep().accept(this);
@ -81,7 +78,6 @@ public class LatexCreator implements StepVisitor {
private String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions) {
//todo sort entries?
if (typeAssumptions.isEmpty()) {
return "";
} else {

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

@ -36,7 +36,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
private static final String INFER_BUTTON_ID = "inferButton";
private static final String EXAMPLE_BUTTON_ID = "exampleButton";
private static final String LAMBDA_BUTTON_ID = "lambdaButton";
private static final short MAX_INPUT_LENGTH = 1000;
private final TextField inputField;
@ -74,20 +74,19 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
Button lambdaButton = new Button(getTranslation("root.lambda"));
lambdaButton.setId(LAMBDA_BUTTON_ID);
UI.getCurrent().getPage().executeJs("window.lambdaButtonListener($0, $1);", LAMBDA_BUTTON_ID, INPUT_FIELD_ID);
typeAssumptions = new Button(
getTranslation("root.typeAssumptions"),
event -> onTypeAssumptionsButton()
);
typeAssumptions = new Button("", event -> onTypeAssumptionsButton());
typeAssumptionsArea = new TypeAssumptionsArea();
Button exampleButton = new Button(getTranslation("root.examplebutton"), event -> onExampleButtonClick());
exampleButton.setId(EXAMPLE_BUTTON_ID);
inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback));
inferTypeButton = new Button("", event -> onTypeInferButtonClick(callback));
inferTypeButton.addClickShortcut(Key.ENTER).listenOn(this);
inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY);
inferTypeButton.setId(INFER_BUTTON_ID);
add(infoIcon, typeAssumptions, lambdaButton, inputField, exampleButton, inferTypeButton);
setId(INPUT_BAR_ID);
localeChange(null);
}
/**
@ -102,7 +101,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
/**
* Sets the type assumptions displayed in the type assumptions area.
*
*
* @param typeAssumptions the type assumptions as a map
*/
protected void setTypeAssumptions(Map<String, String> typeAssumptions) {

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

@ -24,7 +24,7 @@ public class MathjaxDisplay extends LitTemplate implements MathjaxAdapter {
* @param latex the LaTeX string to render with MathJax
*/
public MathjaxDisplay(String latex) {
content.add(latex);
content.setText(latex);
}
@Override

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

@ -3,21 +3,33 @@ package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.html.H1;
import com.vaadin.flow.component.html.H2;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
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 class NotFoundView extends VerticalLayout implements LocaleChangeObserver {
private final H1 error404;
private final H2 suggestion;
/**
* Creates a new NotFoundView.
* Initializes a new NotFoundView with an error message.
*/
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");
error404 = new H1();
suggestion = new H2();
add(error404, suggestion); // todo make beautiful
setAlignItems(Alignment.CENTER);
localeChange(null);
}
@Override
public void localeChange(LocaleChangeEvent event) {
error404.setText(getTranslation("root.title404"));
suggestion.setText(getTranslation("root.message404"));
}
}

21
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java
View File

@ -13,7 +13,8 @@ import org.apache.commons.lang3.StringUtils;
import java.util.function.Consumer;
/**
* Represents a single type assumption. Each TypeAssumptionField is displayed in the TypeAssumptionsArea.
* Represents a single type assumption input component.
* Each TypeAssumptionField is displayed in the TypeAssumptionsArea.
*/
@CssImport("./styles/view/main/type-assumption-field.css")
public class TypeAssumptionField extends HorizontalLayout implements LocaleChangeObserver {
@ -31,9 +32,9 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang
private final TextField typeInputField;
/**
* Creates a new TypeAssumptionField with initial values and a Consumer-object to remove this
* type assumption from the {@link edu.kit.typicalc.view.main.TypeAssumptionsArea}.
*
* Creates a new TypeAssumptionField with initial values and a callback to remove this
* type assumption from the {@link TypeAssumptionsArea}.
*
* @param deleteSelf deletes this object from the TypeAssumptionsArea
* @param variable variable of the type assumption
* @param type type of the type assumption
@ -46,26 +47,26 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang
/**
* Creates a new TypeAssumptionField with a Consumer-object to remove this
* type assumption from the {@link edu.kit.typicalc.view.main.TypeAssumptionsArea}.
*
* type assumption from the {@link TypeAssumptionsArea}.
*
* @param deleteSelf deletes this object from the TypeAssumptionsArea
*/
protected TypeAssumptionField(Consumer<TypeAssumptionField> deleteSelf) {
variableInputField = new TextField();
variableInputField.setLabel(getTranslation("root.variable"));
typeInputField = new TextField();
typeInputField.setLabel(getTranslation("root.type"));
Icon minusIcon = new Icon(VaadinIcon.TRASH);
minusIcon.setId(MINUS_ICON_ID);
Button deleteButton = new Button(minusIcon, event -> deleteSelf.accept(this));
deleteButton.setId(ASS_DELETE_BUTTON_ID);
add(variableInputField, typeInputField, deleteButton);
setId(ASSUMPTIONS_FIELD_ID);
localeChange(null);
}
/**
* Gets the variable of the type assumption.
*
*
* @return the variable of the type assumption
*/
protected String getVariable() {
@ -74,7 +75,7 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang
/**
* Gets the type of the type assumption.
*
*
* @return the type of the type assumption
*/
protected String getType() {

20
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java
View File

@ -16,6 +16,7 @@ import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.TreeMap;
import java.util.stream.Collectors;
/**
@ -43,20 +44,20 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
/**
* Creates a new TypeAssumptionsArea with initial type assumptions.
*
*
* @param types map containing the values for the initial type assumptions
*/
protected TypeAssumptionsArea(Map<String, String> types) {
heading = new H3(getTranslation("root.typeAssumptions"));
heading = new H3("");
VerticalLayout layout = new VerticalLayout();
layout.setId(ASS_LAYOUT_ID);
HorizontalLayout buttons = new HorizontalLayout();
buttons.setId(ASS_BUTTONS_ID);
addAssumption = new Button(getTranslation("root.addAssumption"), new Icon(VaadinIcon.PLUS_CIRCLE));
addAssumption = new Button("", new Icon(VaadinIcon.PLUS_CIRCLE));
addAssumption.setIconAfterText(true);
addAssumption.addClickListener(event -> onAddAssumptionClicked());
deleteAll = new Button(getTranslation("root.deleteAll"), new Icon(VaadinIcon.TRASH));
deleteAll = new Button("", new Icon(VaadinIcon.TRASH));
deleteAll.addClickListener(event -> onDeleteAllClick());
deleteAll.setIconAfterText(true);
deleteAll.addThemeVariants(ButtonVariant.LUMO_ERROR);
@ -77,6 +78,8 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
layout.add(heading, buttons, assumptionContainer);
layout.setPadding(false);
add(layout);
localeChange(null);
}
/**
@ -101,15 +104,16 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
}
/**
* Returns the current type assumptions. If multiple type assumptions contain the same variable only the
* oldest type assumption is returned. All other type assumptions are being ignored.
*
* Returns the current type assumptions.
* If multiple type assumptions define the same variable only the first type assumption is returned.
* The map is sorted by the variable names.
*
* @return the current type assumptions as mappings from a variable to a type
*/
protected Map<String, String> getTypeAssumptions() {
return fields.stream()
.collect(Collectors.toMap(TypeAssumptionField::getVariable, TypeAssumptionField::getType,
(existing, replacement) -> existing));
(existing, replacement) -> existing, TreeMap::new));
}
@Override

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

@ -70,6 +70,8 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
setId(UPPER_BAR_ID);
getThemeList().set("dark", true); //TODO remove magic string
setSpacing(false);
localeChange(null);
}
/**
@ -83,15 +85,15 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
}
/**
* Calls the inferTerm method in {@link edu.kit.typicalc.view.main.InputBar} with the provided
* Calls the inferTerm method in {@link InputBar} with the provided
* string as the argument.
*
* @param term the provided string
* @param typeAssumptions type assumptions to use
*/
protected void inferTerm(String term, Map<String, String> typeAssumptions) {
inputBar.inferTerm(term);
inputBar.setTypeAssumptions(typeAssumptions);
inputBar.inferTerm(term);
}
private void routeToStartPage(Consumer<Component> setContent) {

1
src/main/resources/META-INF/services/com.vaadin.flow.server.VaadinServiceInitListener Normal file
View File

@ -0,0 +1 @@
edu.kit.typicalc.Application

2
src/main/resources/language/translation_en.properties
View File

@ -23,6 +23,8 @@ root.addAssumption=Add Type Assumption
root.deleteAll=Delete All
root.variable=Variable
root.type=Type
root.title404=404 - Not Found
root.message404="Try /infer/<term> or type your favourite term into the input field
root.absLetLatex=\
\\begin{prooftree}\