From 92c694b847af5dcdac64d99793cd12c8a4b242e4 Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Sun, 7 Mar 2021 17:09:19 +0100 Subject: [PATCH] Improved type assumptions --- .../model/parser/TypeAssumptionParser.java | 2 +- .../view/main/TypeAssumptionField.java | 36 ++++++++++++++ .../view/main/TypeAssumptionsArea.java | 47 +++++++++++++++---- .../language/translation_de.properties | 2 + .../language/translation_en.properties | 1 + 5 files changed, 78 insertions(+), 10 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java index 5db6504..e250e9f 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java +++ b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java @@ -43,7 +43,7 @@ public class TypeAssumptionParser { return new Result<>(typeAssumptions); } - private Result parseType(String type) { + public Result parseType(String type) { LambdaLexer lexer = new LambdaLexer(type); Result, ParseError> parsedType = parseType(lexer, 0); if (parsedType.isError()) { diff --git a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java index 19ad339..ec591d9 100644 --- a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java +++ b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java @@ -8,6 +8,7 @@ import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.VaadinIcon; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.component.textfield.TextField; +import com.vaadin.flow.data.binder.Binder; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; import edu.kit.typicalc.model.parser.TypeAssumptionParser; @@ -44,6 +45,7 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang '\u2085', '\u2086', '\u2087', '\u2088', '\u2089'); private static final char TAU = '\u03C4'; + private final TypeAssumptionParser parser = new TypeAssumptionParser(); private final TextField variableInputField; private final TextField typeInputField; @@ -79,9 +81,43 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang Button deleteButton = new Button(minusIcon, event -> deleteSelf.accept(this)); deleteButton.setId(ASS_DELETE_BUTTON_ID); deleteButton.setTabIndex(-1); + addValidatior(); add(variableInputField, typeInputField, deleteButton); setId(ASSUMPTIONS_FIELD_ID); } + + /** + * Checks if the current variable matches the defined syntax. + * + * @param variable the variable + * @return true if the variable matches the syntax, false if not + */ + protected boolean hasCorrectVariable(String variable) { + return variable.isEmpty() || TypeAssumptionParser.TYPE_NAME_PATTERN.matcher(variable).matches(); + } + + /** + * Checks if the current type matches the defined syntax. + * + * @param type the type + * @return true if the type matches the syntax, false if not + */ + protected boolean hasCorrectType(String type) { + return type.isEmpty() || parser.parseType(parseBackType(type)).isOk(); + } + + private void addValidatior() { + Binder varBinder = new Binder<>(); + varBinder.forField(variableInputField) + .withValidator(this::hasCorrectVariable, StringUtils.EMPTY) + .bind(o -> variableInputField.getEmptyValue(), null); + variableInputField.setReadOnly(false); + Binder typeBinder = new Binder<>(); + typeBinder.forField(typeInputField) + .withValidator(this::hasCorrectType, StringUtils.EMPTY) + .bind(o -> typeInputField.getEmptyValue(), null); + typeInputField.setReadOnly(false); + } private String parseBackType(String type) { String rawType = type.replace(TAU, 't'); diff --git a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java index 95ca760..7ef831b 100644 --- a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java +++ b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java @@ -1,5 +1,6 @@ package edu.kit.typicalc.view.main; +import com.vaadin.flow.component.Key; import com.vaadin.flow.component.button.Button; import com.vaadin.flow.component.button.ButtonVariant; import com.vaadin.flow.component.dependency.CssImport; @@ -7,6 +8,9 @@ import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H3; import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.VaadinIcon; +import com.vaadin.flow.component.notification.Notification; +import com.vaadin.flow.component.notification.NotificationVariant; +import com.vaadin.flow.component.notification.Notification.Position; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.i18n.LocaleChangeEvent; @@ -43,7 +47,8 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver private final Button addAssumption; private final Button deleteAll; private final Button saveAssumptions; - + private final Notification invalidInputNotification; + private final List fields = new ArrayList<>(); /** @@ -53,7 +58,8 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver */ protected TypeAssumptionsArea(Map types) { heading = new H3(""); - + invalidInputNotification = createInvInputNotification(); + VerticalLayout layout = new VerticalLayout(); layout.setId(ASS_LAYOUT_ID); HorizontalLayout buttons = new HorizontalLayout(); @@ -65,8 +71,9 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver deleteAll.addClickListener(event -> onDeleteAllClick()); deleteAll.setIconAfterText(true); deleteAll.addThemeVariants(ButtonVariant.LUMO_ERROR); - saveAssumptions = new Button(getTranslation("root.save"), event -> this.close()); + saveAssumptions = new Button(getTranslation("root.save"), event -> closeAction()); saveAssumptions.addThemeVariants(ButtonVariant.LUMO_SUCCESS); + saveAssumptions.addClickShortcut(Key.ENTER); buttons.add(addAssumption, deleteAll, saveAssumptions); assumptionContainer = new VerticalLayout(); @@ -76,15 +83,36 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver layout.add(buttons, assumptionContainer); HorizontalLayout headingLayout = makeHeader(); add(headingLayout, layout); + addDialogCloseActionListener(event -> closeAction()); // attach and trigger javascript event listener after reopening the dialog - addOpenedChangeListener(e -> { - if (e.isOpened()) { - fields.forEach(TypeAssumptionField::refresh); - } - } - ); + addOpenedChangeListener(this::onOpenedChange); + } + + private void onOpenedChange(OpenedChangeEvent event) { + if (event.isOpened()) { + fields.forEach(TypeAssumptionField::refresh); + } } + private void closeAction() { + for (TypeAssumptionField field : fields) { + if (!(field.hasCorrectType(field.getType()) && field.hasCorrectVariable(field.getVariable()))) { + invalidInputNotification.open(); + return; + } + } + invalidInputNotification.close(); + this.close(); + } + + private Notification createInvInputNotification() { + Notification notification = new Notification(); + notification.addThemeVariants(NotificationVariant.LUMO_ERROR); + notification.setPosition(Position.TOP_CENTER); + notification.setDuration(5000); // set the duration to 5 seconds + return notification; + } + private HorizontalLayout makeHeader() { HorizontalLayout headingLayout = new HorizontalLayout(); headingLayout.setId(HEADING_LAYOUT_ID); @@ -150,5 +178,6 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver addAssumption.setText(getTranslation("root.addAssumption")); deleteAll.setText(getTranslation("root.deleteAll")); saveAssumptions.setText(getTranslation("root.save")); + invalidInputNotification.setText(getTranslation("root.correctAssumptions")); } } diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index 30df950..44f23af 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -124,6 +124,8 @@ root.text7=Der Teilen-Knopfs wird betätigt, um das entsprechende Dialogfenster root.image8=/carousel/UseExportDialog.png root.text8=In dem Dialogfenster sind der Permalink zur aktuellen Seite, der Latex-Code des Baums und die im Code \ verwendeten Pakete aufgelistet. +root.correctAssumptions=Korrigiere oder lösche die ungültigen Typannahmen (rot hinterlegt) \ +vor dem Schließen des Dialogs. root.copyLatexTooltip=Kopiere LaTeX-code root.drawerToggleTooltip=Ableitungsregeln root.helpIconTooltip=Hilfe und Sprachwechsel diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties index 1746c80..93c9b36 100644 --- a/src/main/resources/language/translation_en.properties +++ b/src/main/resources/language/translation_en.properties @@ -117,6 +117,7 @@ root.text7=The share button is clicked to open up the corresponding dialog. root.image8=/carousel/UseExportDialog.png root.text8=The dialog contains a permalink to the current page, the LaTeX-code of the tree and the packages needed \ to compile the code. +root.correctAssumptions=Correct or delete the invalid type assumptions (red background) before closing the dialog. root.copyLatexTooltip=Copy LaTeX code root.drawerToggleTooltip=Type inference rules root.helpIconTooltip=Help and language switch