From 8f8b9e967df599a015c11831b87bb8cd39721e7c Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Sun, 7 Mar 2021 14:17:21 +0100 Subject: [PATCH 1/5] Use client value for the algorithm --- src/main/java/edu/kit/typicalc/view/main/InputBar.java | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/main/InputBar.java b/src/main/java/edu/kit/typicalc/view/main/InputBar.java index 82c7309..1fc9135 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/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); - inputField.blur(); - callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions())); + UI.getCurrent().getPage() + .executeJs("return document.getElementById($0).shadowRoot.querySelector('input').value", INPUT_FIELD_ID) + .then(String.class, value -> { + inputField.blur(); + callback.accept(Pair.of(value, typeAssumptionsArea.getTypeAssumptions())); + }); } private void onTypeAssumptionsButton() { 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 2/5] 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 From 815b1f0bd989b5382d8b28d8a8254c47ca61a49b Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Sun, 7 Mar 2021 17:20:08 +0100 Subject: [PATCH 3/5] Fix pipeline --- frontend/styles/view/start-page.css | 7 ++++++ .../content/infocontent/StartPageView.java | 23 +++++++++++-------- 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/frontend/styles/view/start-page.css b/frontend/styles/view/start-page.css index 592c51f..63a60d4 100644 --- a/frontend/styles/view/start-page.css +++ b/frontend/styles/view/start-page.css @@ -38,3 +38,10 @@ height: 500px; width: 100%; } + +#startpage-footer { + position: sticky; + bottom: 1em; + background-color: white; + width: 100%; +} diff --git a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java index 1d66dba..1b053ba 100644 --- a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java +++ b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java @@ -35,6 +35,7 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L private static final String CONTROL_PANEL_ID = "controlPanel"; private static final String START_PAGE_ID = "startPage"; private static final String SLIDE_SHOW_ID = "slideShow"; + private static final String FOOTER_ID = "startpage-footer"; private static final String DOT = "."; @@ -62,17 +63,12 @@ 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); @@ -82,13 +78,20 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L 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"); + footer.setId(FOOTER_ID); 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"); From c5d146a1371738b67b3b9e8a8515a2cd39559e18 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 7 Mar 2021 20:24:08 +0100 Subject: [PATCH 4/5] Move styling into CSS --- frontend/src/mathjax-proof-tree.ts | 1 + frontend/styles/view/control-panel.css | 7 ++++ frontend/styles/view/start-page.css | 14 +++++-- frontend/styles/view/type-inference.css | 37 +++++++++---------- .../typicalc/view/content/ControlPanel.java | 6 ++- .../content/infocontent/StartPageView.java | 10 ++--- .../TypeInferenceView.java | 4 -- 7 files changed, 44 insertions(+), 35 deletions(-) create mode 100644 frontend/styles/view/control-panel.css diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index 55a03c3..684679d 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/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'); diff --git a/frontend/styles/view/control-panel.css b/frontend/styles/view/control-panel.css new file mode 100644 index 0000000..ee57071 --- /dev/null +++ b/frontend/styles/view/control-panel.css @@ -0,0 +1,7 @@ +#share { + margin-left: auto; +} + +#last-step { + margin-right: auto; +} diff --git a/frontend/styles/view/start-page.css b/frontend/styles/view/start-page.css index 63a60d4..040ee0c 100644 --- a/frontend/styles/view/start-page.css +++ b/frontend/styles/view/start-page.css @@ -32,6 +32,7 @@ justify-content: center; align-items: center; width: 100%; + height: 100%; } #slideShow { @@ -39,9 +40,14 @@ width: 100%; } -#startpage-footer { - position: sticky; - bottom: 1em; - background-color: white; +#startPage #content { width: 100%; + height: 100%; + align-items: center; +} + +footer { + width: 100%; + padding-bottom: 1em; + background-color: white; } diff --git a/frontend/styles/view/type-inference.css b/frontend/styles/view/type-inference.css index f249cd9..05cc4fa 100644 --- a/frontend/styles/view/type-inference.css +++ b/frontend/styles/view/type-inference.css @@ -1,32 +1,29 @@ #type-inference-view { - width: 100%; - height: 100%; - padding: 0 0 1em; - align-items: center; + width: 100%; + height: 100%; + padding: 0; + align-items: center; } #type-inference-view::before { - margin: 0 !important; + margin: 0 !important; } -#scroller { - width: 100%; - height: 100%; - margin: 0; -} -#content { - display: flex; - flex-direction: column; - height: 100%; - padding: 10px; - box-sizing: border-box; +#type-inference-view #content { + display: flex; + flex-direction: column; + width: 100%; + height: 100%; + padding: 10px; + box-sizing: border-box; + margin-top: 0; } tc-proof-tree { - border-style: solid; - border-color: #37485f; + border-style: solid; + border-color: #37485f; } tc-unification { - background-color: #e9f2fd; -} \ No newline at end of file + background-color: #e9f2fd; +} diff --git a/src/main/java/edu/kit/typicalc/view/content/ControlPanel.java b/src/main/java/edu/kit/typicalc/view/content/ControlPanel.java index 2ae2ee3..bfa5f0c 100644 --- a/src/main/java/edu/kit/typicalc/view/content/ControlPanel.java +++ b/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"); - lastStep.getStyle().set("margin-right", "auto"); + share.setId(SHARE_ID); add(share, firstStep, previousStep, nextStep, lastStep); } diff --git a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java index 1b053ba..e740951 100644 --- a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java +++ b/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"; @@ -49,7 +50,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); @@ -73,16 +77,12 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L 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.setId(FOOTER_ID); - content.setWidthFull(); add(content, footer); } - + private Div createTextContainer() { Div textContainer = new Div(); textContainer.setId(TEXT_CONTAINER_ID); diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index 784578c..aabb5e5 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java @@ -69,10 +69,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); } From ac932a6e0c51ffa61f5e151c99130ec33d0f5b4a Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 7 Mar 2021 21:31:50 +0100 Subject: [PATCH 5/5] Fix page title not updating --- .../edu/kit/typicalc/presenter/Presenter.java | 6 -- .../content/infocontent/StartPageView.java | 1 - .../TypeInferenceView.java | 52 +++++++++++++--- .../kit/typicalc/view/main/MainViewImpl.java | 61 +++++++------------ .../edu/kit/typicalc/view/main/UpperBar.java | 23 +++---- 5 files changed, 74 insertions(+), 69 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/presenter/Presenter.java b/src/main/java/edu/kit/typicalc/presenter/Presenter.java index 5e36082..22d6065 100644 --- a/src/main/java/edu/kit/typicalc/presenter/Presenter.java +++ b/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 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 result = model.getTypeInferer(lambdaTerm, typeAssumptions); if (result.isError()) { view.displayError(result.unwrapError()); diff --git a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java index e740951..0e4b540 100644 --- a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java +++ b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java @@ -36,7 +36,6 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L private static final String CONTROL_PANEL_ID = "controlPanel"; private static final String START_PAGE_ID = "startPage"; private static final String SLIDE_SHOW_ID = "slideShow"; - private static final String FOOTER_ID = "startpage-footer"; private static final String DOT = "."; diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index aabb5e5..51804d8 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/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, LocaleChangeObserver { + implements ControlPanelView, ComponentEventListener, 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 @@ -138,11 +156,31 @@ public class TypeInferenceView extends VerticalLayout @Override public void localeChange(LocaleChangeEvent localeChangeEvent) { - lc = new LatexCreator(typeInferer, - error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH))); - unification = new MathjaxUnification(lc.getUnification()); - content.removeAll(); - content.add(unification, tree); - refreshElements(); + if (typeInferer != null) { + lc = new LatexCreator(typeInferer, + error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH))); + unification = new MathjaxUnification(lc.getUnification()); + content.removeAll(); + 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; } } diff --git a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java index abb9553..f1c437c 100644 --- a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java +++ b/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 { + implements MainView, HasErrorParameter, 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 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(tiv.get()); + setContent(new TypeInferenceView(typeInferer)); } @Override @@ -70,56 +68,41 @@ public class MainViewImpl extends AppLayout } @Override - public void beforeEnter(BeforeEnterEvent event) { - tiv = Optional.empty(); - if (event.getLocation().getPath().matches(TypeInferenceView.ROUTE + "/.*")) { - Location url = event.getLocation(); + public void afterNavigation(AfterNavigationEvent event) { + this.handleLocation(event.getLocation()); + } + + private void handleLocation(Location url) { + if (url.getPath().matches(TypeInferenceView.ROUTE + "/.*")) { List segments = url.getSegments(); String term = segments.get(segments.size() - 1); Map 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 - protected void afterNavigation() { - // this method ensures that the content is visible after navigation - tiv.ifPresent(this::setContent); - } - - private void setTermInURL(Pair> lambdaTermAndAssumptions) { + private void processInput(Pair> lambdaTermAndAssumptions) { String lambdaTerm = lambdaTermAndAssumptions.getLeft(); - if ("".equals(lambdaTerm)) { - UI.getCurrent().getPage().getHistory().pushState(null, "./"); - setContent(new StartPageView()); + if (lambdaTerm.isBlank()) { + UI.getCurrent().navigate("./"); return; } - StringBuilder types = new StringBuilder(); - for (Map.Entry type : lambdaTermAndAssumptions.getRight().entrySet()) { - if (types.length() > 0) { - types.append('&'); - } - 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)); + QueryParameters qp = new QueryParameters(lambdaTermAndAssumptions.getRight().entrySet().stream().map(entry -> + Pair.of(entry.getKey(), List.of(entry.getValue())) + ).collect(Collectors.toMap(Pair::getLeft, Pair::getRight, + (existing, replacement) -> existing, TreeMap::new))); + UI.getCurrent().navigate(TypeInferenceView.ROUTE + "/" + lambdaTerm, qp); } private String decodeURL(String encodedUrl) { - return java.net.URLDecoder.decode(encodedUrl, StandardCharsets.UTF_8); + return URLDecoder.decode(encodedUrl, StandardCharsets.UTF_8); } @Override diff --git a/src/main/java/edu/kit/typicalc/view/main/UpperBar.java b/src/main/java/edu/kit/typicalc/view/main/UpperBar.java index 10751df..1c3279d 100644 --- a/src/main/java/edu/kit/typicalc/view/main/UpperBar.java +++ b/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>> setTermInURL; + private final transient Consumer>> 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>> setTermInURL) { + protected UpperBar(MainViewListener presenter, Consumer>> 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> termAndAssumptions) { - setTermInURL.accept(termAndAssumptions); - if (!"".equals(termAndAssumptions.getLeft())) { - startInfer(termAndAssumptions.getLeft(), termAndAssumptions.getRight()); - } + inputConsumer.accept(termAndAssumptions); } private void startInfer(String term, Map 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"));