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

frontend/src/mathjax-proof-tree.ts

@@ -48,6 +48,7 @@ class MathjaxProofTree extends MathjaxAdapter {
         const stepSelector = 'g[typicalc="step"]';
         // space between inference premises
         const padding = 300;
+        console.log("calculating steps..");
 
         if (this.shadowRoot !== null) {
             console.time('stepCalculation');

frontend/styles/view/control-panel.css

@@ -0,0 +1,7 @@
+#share {
+    margin-left: auto;
+}
+
+#last-step {
+    margin-right: auto;
+}

frontend/styles/view/start-page.css

@@ -32,9 +32,22 @@
 	justify-content: center;
 	align-items: center;
 	width: 100%;
+	height: 100%;
 }
 
 #slideShow {
 	height: 500px;
 	width: 100%;
 }
+
+#startPage #content {
+	width: 100%;
+	height: 100%;
+	align-items: center;
+}
+
+footer {
+	width: 100%;
+	padding-bottom: 1em;
+	background-color: white;
+}

frontend/styles/view/type-inference.css

@@ -1,32 +1,29 @@
 #type-inference-view {
-    width: 100%;
+	width: 100%;
-    height: 100%;
+	height: 100%;
-    padding: 0 0 1em;
+	padding: 0;
-    align-items: center;
+	align-items: center;
 }
 
 #type-inference-view::before {
-    margin: 0 !important;
+	margin: 0 !important;
 }
 
-#scroller {
+#type-inference-view #content {
-    width: 100%;
+	display: flex;
-    height: 100%;
+	flex-direction: column;
-    margin: 0;
+	width: 100%;
-}
+	height: 100%;
-#content {
+	padding: 10px;
-    display: flex;
+	box-sizing: border-box;
-    flex-direction: column;
+	margin-top: 0;
-    height: 100%;
-    padding: 10px;
-    box-sizing: border-box;
 }
 
 tc-proof-tree {
-    border-style: solid;
+	border-style: solid;
-    border-color: #37485f;
+	border-color: #37485f;
 }
 
 tc-unification {
-    background-color: #e9f2fd;
+	background-color: #e9f2fd;
-}
+}

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/presenter/Presenter.java

@@ -2,7 +2,6 @@ package edu.kit.typicalc.presenter;
 
 import java.util.Map;
 
-import com.vaadin.flow.component.UI;
 import edu.kit.typicalc.model.Model;
 import edu.kit.typicalc.model.TypeInfererInterface;
 import edu.kit.typicalc.model.parser.ParseError;
@@ -31,11 +30,6 @@ public class Presenter implements MainViewListener {
 
     @Override
     public void typeInferLambdaString(String lambdaTerm, Map<String, String> typeAssumptions) {
-        if (lambdaTerm.isBlank()) {
-            UI.getCurrent().getPage().setTitle(UI.getCurrent().getTranslation("root.typicalc"));
-        } else {
-            UI.getCurrent().getPage().setTitle(UI.getCurrent().getTranslation("root.typicalc") + " - " + lambdaTerm);
-        }
         Result<TypeInfererInterface, ParseError> result = model.getTypeInferer(lambdaTerm, typeAssumptions);
         if (result.isError()) {
             view.displayError(result.unwrapError());

src/main/java/edu/kit/typicalc/view/content/ControlPanel.java

@@ -1,6 +1,7 @@
 package edu.kit.typicalc.view.content;
 
 import com.vaadin.flow.component.button.Button;
+import com.vaadin.flow.component.dependency.CssImport;
 import com.vaadin.flow.component.icon.Icon;
 import com.vaadin.flow.component.icon.VaadinIcon;
 import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
@@ -10,6 +11,7 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
 /**
  * Provides a GUI in form of buttons for the user to navigate through steps.
  */
+@CssImport("./styles/view/control-panel.css")
 public class ControlPanel extends HorizontalLayout implements LocaleChangeObserver {
 
     private static final String ATTRIBUTE_TITLE = "title";
@@ -25,6 +27,7 @@ public class ControlPanel extends HorizontalLayout implements LocaleChangeObserv
     private final Button previousStep;
     private static final String PREVIOUS_STEP_ID = "previous-step";
     private final Button share;
+    private static final String SHARE_ID = "share";
 
     /**
      * Sets up buttons with click-listeners that call the corresponding method in the view.
@@ -42,8 +45,7 @@ public class ControlPanel extends HorizontalLayout implements LocaleChangeObserv
         previousStep = new Button(new Icon(VaadinIcon.ANGLE_LEFT), evt -> view.previousStepButton());
         previousStep.setId(PREVIOUS_STEP_ID);
         share = new Button(new Icon(VaadinIcon.CONNECT), evt -> view.shareButton());
-        share.getStyle().set("margin-left", "auto");
+        share.setId(SHARE_ID);
-        lastStep.getStyle().set("margin-right", "auto");
 
         add(share, firstStep, previousStep, nextStep, lastStep);
     }

src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java

@@ -27,6 +27,7 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
 
     private static final long serialVersionUID = 2502750919087936406L;
 
+    private static final String CONTENT_ID = "content";
     private static final String HEADING_ID = "startPage-Heading";
     private static final String H_LINE_ID = "horizontalLine";
     private static final String TEXT_CONTAINER_ID = "textContainer";
@@ -48,7 +49,10 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
      * Fills the view with content.
      */
     public StartPageView() {
+        setId(START_PAGE_ID);
+
         VerticalLayout content = new VerticalLayout();
+        content.setId(CONTENT_ID);
         ControlPanel controlPanel = new ControlPanel(this);
         controlPanel.setId(CONTROL_PANEL_ID);
         controlPanel.setEnabledShareButton(false);
@@ -62,34 +66,32 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
         line1.setId(H_LINE_ID);
         Hr line2 = new Hr();
         line2.setId(H_LINE_ID);
-        Div textContainer = new Div();
-        textContainer.setId(TEXT_CONTAINER_ID);
         introduction = new Span();
 
         linkText = new Text(getTranslation("root.linkText"));
         link = new Anchor(getTranslation("root.link"), getTranslation("root.here"));
-        link.setTarget("_blank"); // opens new tab
-        Paragraph linkContainer = new Paragraph(linkText, link, new Text(DOT));
-        linkContainer.setId(LINK_CONTAINER_ID);
 
-        textContainer.add(introduction, linkContainer);
+        Div textContainer = createTextContainer();
 
         slideProgress = new ProgressBar(slideShow.getStartPosition(), slideShow.getSlides().length - 1);
         slideProgress.setId(SLIDE_PROGRESS_ID);
 
-        content.setAlignItems(Alignment.CENTER);
         content.add(heading, line1, textContainer, slideProgress, slideShow, line2);
-        setId(START_PAGE_ID);
 
         Footer footer = new Footer(controlPanel);
-        footer.setWidthFull();
-        footer.getStyle().set("position", "sticky");
-        footer.getStyle().set("bottom", "1em");
-        footer.getStyle().set("background-color", "white");
-        content.setWidthFull();
         add(content, footer);
     }
 
+    private Div createTextContainer() {
+        Div textContainer = new Div();
+        textContainer.setId(TEXT_CONTAINER_ID);
+        link.setTarget("_blank"); // opens new tab
+        Paragraph linkContainer = new Paragraph(linkText, link, new Text(DOT));
+        linkContainer.setId(LINK_CONTAINER_ID);
+        textContainer.add(introduction, linkContainer);
+        return textContainer;
+    }
+
     private Carousel createScenarioCarousel() {
         Slide slide1 = new ImageSlide(getTranslation("root.image1"), "root.text1");
         Slide slide2 = new ImageSlide(getTranslation("root.image2"), "root.text2");

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

@@ -10,11 +10,18 @@ import com.vaadin.flow.component.html.Footer;
 import com.vaadin.flow.component.orderedlayout.VerticalLayout;
 import com.vaadin.flow.i18n.LocaleChangeEvent;
 import com.vaadin.flow.i18n.LocaleChangeObserver;
+import com.vaadin.flow.router.BeforeEnterEvent;
+import com.vaadin.flow.router.BeforeEnterObserver;
+import com.vaadin.flow.router.HasDynamicTitle;
+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.content.typeinferencecontent.latexcreator.LatexCreator;
+import edu.kit.typicalc.view.main.MainViewImpl;
 
+import java.net.URLDecoder;
+import java.nio.charset.StandardCharsets;
 import java.util.List;
 import java.util.Locale;
 
@@ -27,8 +34,10 @@ import java.util.Locale;
  */
 @CssImport("./styles/view/type-inference.css")
 @JavaScript("./src/key-shortcuts.js")
+@Route(value = TypeInferenceView.ROUTE + "/:term", layout = MainViewImpl.class)
 public class TypeInferenceView extends VerticalLayout
-        implements ControlPanelView, ComponentEventListener<AttachEvent>, LocaleChangeObserver {
+        implements ControlPanelView, ComponentEventListener<AttachEvent>, LocaleChangeObserver, HasDynamicTitle,
+        BeforeEnterObserver {
     /**
      * Route of this view.
      */
@@ -47,6 +56,15 @@ public class TypeInferenceView extends VerticalLayout
     private final transient TypeInfererInterface typeInferer;
     private final Div content;
     private final ControlPanel controlPanel;
+    private String term = "?";
+
+    // used by Spring
+    public TypeInferenceView() {
+        this.typeInferer = null;
+        this.content = null;
+        this.controlPanel = null;
+        this.treeNumbers = null;
+    }
 
     /**
      * Initializes the component. When initialization is complete, the first step of the type
@@ -69,10 +87,6 @@ public class TypeInferenceView extends VerticalLayout
         controlPanel.setEnabledPreviousStep(false);
 
         Footer footer = new Footer(controlPanel);
-        footer.getStyle().set("position", "sticky");
-        footer.getStyle().set("bottom", "1em");
-        content.getStyle().set("overflow", "auto");
-        content.setWidthFull();
         add(content, footer);
     }
 
@@ -142,11 +156,31 @@ public class TypeInferenceView extends VerticalLayout
 
     @Override
     public void localeChange(LocaleChangeEvent localeChangeEvent) {
-        lc = new LatexCreator(typeInferer,
+        if (typeInferer != null) {
-                error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)));
+            lc = new LatexCreator(typeInferer,
-        unification = new MathjaxUnification(lc.getUnification());
+                    error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)));
-        content.removeAll();
+            unification = new MathjaxUnification(lc.getUnification());
-        content.add(unification, tree);
+            content.removeAll();
-        refreshElements();
+            content.add(unification, tree);
+            refreshElements();
+        }
+    }
+
+    @Override
+    public void beforeEnter(BeforeEnterEvent event) {
+        if (event.getLocation().getPath().matches(ROUTE + "/.*")) {
+            term = URLDecoder.decode(
+                    event.getRouteParameters().get("term")
+                            .orElseThrow(IllegalStateException::new),
+                    StandardCharsets.UTF_8);
+        }
+    }
+
+    @Override
+    public String getPageTitle() {
+        if (typeInferer != null) {
+            return typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm().toString();
+        }
+        return UI.getCurrent().getTranslation("root.typicalc") + " - " + term;
     }
 }

src/main/java/edu/kit/typicalc/view/main/InputBar.java

@@ -13,7 +13,6 @@ import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
 import com.vaadin.flow.component.textfield.TextField;
 import com.vaadin.flow.i18n.LocaleChangeEvent;
 import com.vaadin.flow.i18n.LocaleChangeObserver;
-import org.apache.commons.lang3.StringUtils;
 import org.apache.commons.lang3.tuple.Pair;
 
 import java.util.Map;
@@ -118,9 +117,12 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
     }
 
     private void onTypeInferButtonClick() {
-        String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY);
+        UI.getCurrent().getPage()
-        inputField.blur();
+            .executeJs("return document.getElementById($0).shadowRoot.querySelector('input').value", INPUT_FIELD_ID)
-        callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions()));
+            .then(String.class, value -> {
+                inputField.blur();
+                callback.accept(Pair.of(value, typeAssumptionsArea.getTypeAssumptions()));
+            });
     }
 
     private void onTypeAssumptionsButton() {

src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java

@@ -16,11 +16,12 @@ import org.apache.commons.lang3.StringUtils;
 import org.apache.commons.lang3.tuple.Pair;
 
 import javax.servlet.http.HttpServletResponse;
+import java.net.URLDecoder;
 import java.nio.charset.StandardCharsets;
 import java.util.Collections;
 import java.util.List;
 import java.util.Map;
-import java.util.Optional;
+import java.util.TreeMap;
 import java.util.stream.Collectors;
 
 /**
@@ -34,9 +35,8 @@ import java.util.stream.Collectors;
 @CssImport(value = "./styles/view/main/app-layout.css", themeFor = "vaadin-app-layout")
 @JavaScript("./src/svg-pan-zoom.min.js")
 @JavaScript("./src/tex-svg-full.js")
-@Route(TypeInferenceView.ROUTE + "/:term")
 public class MainViewImpl extends AppLayout
-        implements MainView, BeforeEnterObserver, HasErrorParameter<NotFoundException> {
+        implements MainView, HasErrorParameter<NotFoundException>, AfterNavigationObserver {
     private static final long serialVersionUID = -2411433187835906976L;
 
     /**
@@ -45,7 +45,6 @@ public class MainViewImpl extends AppLayout
     public static final String PAGE_TITLE = "Typicalc";
 
     private final UpperBar upperBar;
-    private transient Optional<TypeInferenceView> tiv = Optional.empty();
 
     /**
      * Creates a new MainViewImpl.
@@ -53,15 +52,14 @@ public class MainViewImpl extends AppLayout
     public MainViewImpl() {
         setDrawerOpened(false);
         MainViewListener presenter = new Presenter(new ModelImpl(), this);
-        upperBar = new UpperBar(presenter, this::setTermInURL);
+        upperBar = new UpperBar(presenter, this::processInput);
         addToNavbar(upperBar);
         addToDrawer(new DrawerContent());
     }
 
     @Override
     public void setTypeInferenceView(TypeInfererInterface typeInferer) {
-        tiv = Optional.of(new TypeInferenceView(typeInferer));
+        setContent(new TypeInferenceView(typeInferer));
-        setContent(tiv.get());
     }
 
     @Override
@@ -70,56 +68,41 @@ public class MainViewImpl extends AppLayout
     }
 
     @Override
-    public void beforeEnter(BeforeEnterEvent event) {
+    public void afterNavigation(AfterNavigationEvent event) {
-        tiv = Optional.empty();
+        this.handleLocation(event.getLocation());
-        if (event.getLocation().getPath().matches(TypeInferenceView.ROUTE + "/.*")) {
+    }
-            Location url = event.getLocation();
+
+    private void handleLocation(Location url) {
+        if (url.getPath().matches(TypeInferenceView.ROUTE + "/.*")) {
             List<String> segments = url.getSegments();
             String term = segments.get(segments.size() - 1);
             Map<String, String> types = url.getQueryParameters().getParameters().entrySet().stream().map(entry ->
                     Pair.of(entry.getKey(), entry.getValue().get(0))
             ).collect(Collectors.toMap(Pair::getLeft, Pair::getRight));
             upperBar.inferTerm(decodeURL(term), types);
-        } else if (event.getLocation().getPath().equals(TypeInferenceView.ROUTE)) {
+        } else if (url.getPath().equals(TypeInferenceView.ROUTE)) {
             setContent(new StartPageView());
             upperBar.inferTerm(StringUtils.EMPTY, Collections.emptyMap());
-        } else if (event.getLocation().getPath().equals(StringUtils.EMPTY)) {
+        } else if (url.getPath().equals(StringUtils.EMPTY)) {
             setContent(new StartPageView());
         }
     }
 
-    @Override
+    private void processInput(Pair<String, Map<String, String>> lambdaTermAndAssumptions) {
-    protected void afterNavigation() {
-        // this method ensures that the content is visible after navigation
-        tiv.ifPresent(this::setContent);
-    }
-
-    private void setTermInURL(Pair<String, Map<String, String>> lambdaTermAndAssumptions) {
         String lambdaTerm = lambdaTermAndAssumptions.getLeft();
-        if ("".equals(lambdaTerm)) {
+        if (lambdaTerm.isBlank()) {
-            UI.getCurrent().getPage().getHistory().pushState(null, "./");
+            UI.getCurrent().navigate("./");
-            setContent(new StartPageView());
             return;
         }
-        StringBuilder types = new StringBuilder();
+        QueryParameters qp = new QueryParameters(lambdaTermAndAssumptions.getRight().entrySet().stream().map(entry ->
-        for (Map.Entry<String, String> type : lambdaTermAndAssumptions.getRight().entrySet()) {
+                Pair.of(entry.getKey(), List.of(entry.getValue()))
-            if (types.length() > 0) {
+        ).collect(Collectors.toMap(Pair::getLeft, Pair::getRight,
-                types.append('&');
+                (existing, replacement) -> existing, TreeMap::new)));
-            }
+        UI.getCurrent().navigate(TypeInferenceView.ROUTE + "/" + lambdaTerm, qp);
-            types.append(type.getKey());
-            types.append('=');
-            types.append(type.getValue());
-        }
-        String typeAssumptions = "";
-        if (types.length() > 0) {
-            typeAssumptions = "?" + types.toString();
-        }
-        UI.getCurrent().getPage().getHistory().pushState(null,
-                new Location(TypeInferenceView.ROUTE + "/" + lambdaTerm + typeAssumptions));
     }
 
     private String decodeURL(String encodedUrl) {
-        return java.net.URLDecoder.decode(encodedUrl, StandardCharsets.UTF_8);
+        return URLDecoder.decode(encodedUrl, StandardCharsets.UTF_8);
     }
 
     @Override

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<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');

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<TypeAssumptionField> fields = new ArrayList<>();
 
     /**
@@ -53,7 +58,8 @@ 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);
         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 -> {
+        addOpenedChangeListener(this::onOpenedChange);
-           if (e.isOpened()) { 
+    }
-                   fields.forEach(TypeAssumptionField::refresh); 
+    
-               } 
+    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() {
         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"));
     }
 }

src/main/java/edu/kit/typicalc/view/main/UpperBar.java

@@ -3,7 +3,6 @@ package edu.kit.typicalc.view.main;
 import com.vaadin.flow.component.applayout.DrawerToggle;
 import com.vaadin.flow.component.button.Button;
 import com.vaadin.flow.component.dependency.CssImport;
-import com.vaadin.flow.component.dialog.Dialog;
 import com.vaadin.flow.component.html.Anchor;
 import com.vaadin.flow.component.html.H1;
 import com.vaadin.flow.component.icon.Icon;
@@ -39,20 +38,20 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
     private final InputBar inputBar;
     private final Button toggle;
     private final Button helpButton;
-    
+
     private final transient MainViewListener presenter;
-    private final transient Consumer<Pair<String, Map<String, String>>> setTermInURL;
+    private final transient Consumer<Pair<String, Map<String, String>>> inputConsumer;
 
     /**
      * Initializes a new UpperBar with the provided mainViewListener.
      *
      * @param presenter    the listener used to communicate with the model
-     * @param setTermInURL function to set the term into the URL
+     * @param inputConsumer function to handle user input
      */
-    protected UpperBar(MainViewListener presenter, Consumer<Pair<String, Map<String, String>>> setTermInURL) {
+    protected UpperBar(MainViewListener presenter, Consumer<Pair<String, Map<String, String>>> inputConsumer) {
 
         this.presenter = presenter;
-        this.setTermInURL = setTermInURL;
+        this.inputConsumer = inputConsumer;
 
         toggle = new DrawerToggle();
         H1 viewTitle = new H1(new Anchor("/", getTranslation("root.typicalc")));
@@ -60,7 +59,7 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
         this.inputBar = new InputBar(this::typeInfer);
         inputBar.setId(INPUT_BAR_ID);
         helpButton = new Button(new Icon(VaadinIcon.QUESTION_CIRCLE));
-        helpButton.addClickListener(event -> onHelpIconClick());
+        helpButton.addClickListener(event -> new HelpDialog().open());
         helpButton.setId(HELP_ICON_ID);
 
         add(toggle, viewTitle, inputBar, helpButton);
@@ -76,10 +75,7 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
      * @param termAndAssumptions the lambda term to be type-inferred and the type assumptions to use
      */
     protected void typeInfer(Pair<String, Map<String, String>> termAndAssumptions) {
-        setTermInURL.accept(termAndAssumptions);
+        inputConsumer.accept(termAndAssumptions);
-        if (!"".equals(termAndAssumptions.getLeft())) {
-            startInfer(termAndAssumptions.getLeft(), termAndAssumptions.getRight());
-        }
     }
 
     private void startInfer(String term, Map<String, String> typeAssumptions) {
@@ -98,11 +94,6 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
         startInfer(term, typeAssumptions);
     }
 
-    private void onHelpIconClick() {
-        Dialog helpDialog = new HelpDialog();
-        helpDialog.open();
-    }
-
     @Override
     public void localeChange(LocaleChangeEvent event) {
         toggle.getElement().setAttribute("title", getTranslation("root.drawerToggleTooltip"));

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