Improved type assumptions

src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java

@@ -43,7 +43,7 @@ public class TypeAssumptionParser {
         return new Result<>(typeAssumptions);
     }
 
-    private Result<TypeAbstraction, ParseError> parseType(String type) {
+    public Result<TypeAbstraction, ParseError> parseType(String type) {
         LambdaLexer lexer = new LambdaLexer(type);
         Result<Pair<Type, Integer>, ParseError> parsedType = parseType(lexer, 0);
         if (parsedType.isError()) {

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,10 +81,44 @@ 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<String> varBinder = new Binder<>();
+        varBinder.forField(variableInputField)
+                .withValidator(this::hasCorrectVariable, StringUtils.EMPTY)
+                .bind(o -> variableInputField.getEmptyValue(), null);
+        variableInputField.setReadOnly(false);
+        Binder<String> 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');
         char[] rawTypeArray = rawType.toCharArray();

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,6 +47,7 @@ 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<TypeAssumptionField> fields = new ArrayList<>();
 
@@ -53,6 +58,7 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
      */
     protected TypeAssumptionsArea(Map<String, String> types) {
         heading = new H3("");
+        invalidInputNotification = createInvInputNotification();
             
         VerticalLayout layout = new VerticalLayout();
         layout.setId(ASS_LAYOUT_ID);
@@ -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,13 +83,34 @@ 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()) { 
+        addOpenedChangeListener(this::onOpenedChange);
+    }
+    
+    private void onOpenedChange(OpenedChangeEvent<Dialog> 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() {
@@ -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"));
     }
 }

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

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