From c9512b57d283163f930eea1e09a36637b96a93d0 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 6 Feb 2021 10:41:06 +0100 Subject: [PATCH 1/4] Fix display of inference tree after reload --- src/main/java/edu/kit/typicalc/view/main/InputBar.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 c7757dd..a1afcda 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -1,6 +1,7 @@ package edu.kit.typicalc.view.main; import com.vaadin.flow.component.Key; +import com.vaadin.flow.component.UI; import com.vaadin.flow.component.button.Button; import com.vaadin.flow.component.button.ButtonVariant; import com.vaadin.flow.component.dependency.CssImport; @@ -81,7 +82,10 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { */ protected void inferTerm(String term) { inputField.setValue(term); - inferTypeButton.click(); + // for some reason the Vaadin "click" does not work + //inferTypeButton.click(); + UI.getCurrent().getPage().executeJs( + String.format("document.getElementById('%s').click()", INFER_BUTTON_ID)); } private void onInputFieldValueChange() { From 843430439dc7d2c6f2c1c0db1939301c4d8f2109 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 6 Feb 2021 10:41:28 +0100 Subject: [PATCH 2/4] Fix layout of upper bar --- frontend/src/mathjax-proof-tree.ts | 11 ++++++----- frontend/styles/view/main/input-bar.css | 13 +++---------- frontend/styles/view/main/upper-bar.css | 26 ++++--------------------- 3 files changed, 13 insertions(+), 37 deletions(-) diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index 8ea64d1..324e7f3 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/frontend/src/mathjax-proof-tree.ts @@ -26,9 +26,10 @@ class MathjaxProofTree extends MathjaxAdapter { protected calculateSteps(): void { if (this.shadowRoot !== null) { + const root = this.shadowRoot; let semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0; // first, enumerate all of the steps - let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT); + let nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT); let steps = []; let a = null; let stepIdx = 0; @@ -44,7 +45,7 @@ class MathjaxProofTree extends MathjaxAdapter { } } // then fix some more mathjax layout issues - for (const step of this.shadowRoot.querySelectorAll('g[typicalc="step"]')) { + for (const step of root.querySelectorAll('g[typicalc="step"]')) { const infRule = step.querySelector('g[semantics="bspr_inferenceRule:down"]'); if (infRule === null) { continue; @@ -78,7 +79,7 @@ class MathjaxProofTree extends MathjaxAdapter { stepAbove.transform.baseVal[0].matrix.e -= dx; } // then create the steps - nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT); + nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT); steps = []; stepIdx = 0; while (a = nodeIterator.nextNode() as HTMLElement) { @@ -122,7 +123,7 @@ class MathjaxProofTree extends MathjaxAdapter { steps.push([a, above]); } } - const svg = this.shadowRoot.querySelector("svg")!; + const svg = root.querySelector("svg")!; const nodeIterator2 = [...svg.querySelectorAll("g[data-mml-node='mtr']")]; // start layout fixes in the innermost part of the SVG nodeIterator2.reverse(); @@ -170,8 +171,8 @@ class MathjaxProofTree extends MathjaxAdapter { i += 1; } } - const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox(); // TODO: this does not work when using a permalink + const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox(); svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height); if (counter >= 3) { // should not be used on empty SVGs diff --git a/frontend/styles/view/main/input-bar.css b/frontend/styles/view/main/input-bar.css index 0c164b3..37a9b0c 100644 --- a/frontend/styles/view/main/input-bar.css +++ b/frontend/styles/view/main/input-bar.css @@ -1,13 +1,5 @@ -@media (max-width: 500px) { - #inputField { - width: 20em; - } -} - -@media (min-width: 1000px) { - #inputField { - width: 30em; - } +#inputField { + flex-grow: 1; } #inputField { @@ -16,6 +8,7 @@ #inputBar { align-items: center; + padding: 1em; } vaadin-drawer-toggle { diff --git a/frontend/styles/view/main/upper-bar.css b/frontend/styles/view/main/upper-bar.css index cbc2493..d311ca2 100644 --- a/frontend/styles/view/main/upper-bar.css +++ b/frontend/styles/view/main/upper-bar.css @@ -19,31 +19,13 @@ } #helpIcon { - margin-left: auto; + margin-left: 1em; margin-right: 1em; } -@media (max-width: 500px) { - #inputBar { - margin: auto; - } - - #viewTitle { - margin-right: 5em; - } -} - -@media (min-width: 1000px) { - #inputBar { - margin-left: 15em; - } - - #viewTitle { - margin-right: auto; - } +#inputBar { + flex-grow: 1; + justify-content: end; } - - - From d3fd5b99a83c3de4290e5a15c3c875d9cf177240 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 6 Feb 2021 10:57:35 +0100 Subject: [PATCH 3/4] Set page title to lambda term --- frontend/src/mathjax-proof-tree.ts | 6 +++--- src/main/java/edu/kit/typicalc/view/main/InputBar.java | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index 324e7f3..5365670 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/frontend/src/mathjax-proof-tree.ts @@ -171,9 +171,9 @@ class MathjaxProofTree extends MathjaxAdapter { i += 1; } } - // TODO: this does not work when using a permalink - const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox(); - svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height); + // TODO: this does not scale the SVG correctly + //const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox(); + //svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height); if (counter >= 3) { // should not be used on empty SVGs // @ts-ignore 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 a1afcda..f348a0f 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -97,6 +97,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY); if (currentInput.length() < MAX_INPUT_LENGTH) { + UI.getCurrent().getPage().setTitle(getTranslation("root.typicalc") + " - " + currentInput); callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions())); } else { final Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput")); From 6fa50cbf31df26a851c34e97ff8a1ae200fa9336 Mon Sep 17 00:00:00 2001 From: Johanna Stuber Date: Sat, 6 Feb 2021 10:58:12 +0100 Subject: [PATCH 4/4] delete todo and comment, make long example inferrable --- src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java | 3 --- src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java | 2 +- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java index 560e5fc..d565f40 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java @@ -63,9 +63,6 @@ public class TypeInferenceResult { } } return typeVar; - // TODO: correct? -// throw new IllegalStateException("MGU has to contain substitution for original type variable: " -// + typeVar.toString()); } /** diff --git a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java index 1dd36be..594fe57 100644 --- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java @@ -23,7 +23,7 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver { private static final List EXAMPLES = List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)", - "(λx.λy.y (x x)) (λz. λa. z g a)"); + "(λx.λy.y (x y)) (λz. λa. z g a)"); private final Paragraph instruction; /**