From 5a1aaa8408b8008f208788bdca64eac0b854ab11 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 10 Mar 2021 17:09:20 +0100 Subject: [PATCH 1/5] Fix NPE in TypeInferenceView --- .../view/content/typeinferencecontent/TypeInferenceView.java | 1 + 1 file changed, 1 insertion(+) 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 ef291f4..167e096 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 @@ -185,6 +185,7 @@ public class TypeInferenceView extends VerticalLayout content.removeAll(); lc = new LatexCreator(typeInferer, error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH))); + treeNumbers = lc.getTreeNumbers(); setContent(); refreshElements(); } From b3155039754468aabb91a132522b04a09ab883de Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 10 Mar 2021 17:33:16 +0100 Subject: [PATCH 2/5] Fix production build --- pom.xml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/pom.xml b/pom.xml index 01daf37..0af25b3 100644 --- a/pom.xml +++ b/pom.xml @@ -1,5 +1,7 @@ - + 4.0.0 edu.kit.typicalc typicalc @@ -280,10 +282,12 @@ - + Date: Wed, 10 Mar 2021 18:04:32 +0100 Subject: [PATCH 3/5] Optimize frontend calls --- frontend/src/input-bar-enhancements.js | 31 +++++++++++++++++++ frontend/src/lambda-button-listener.js | 10 ------ frontend/src/mathjax-adapter.ts | 10 ++---- frontend/src/mathjax-display.ts | 5 ++- frontend/src/mathjax-unification.ts | 6 +++- frontend/styles/view/type-inference.css | 2 +- .../MathjaxProofTree.java | 7 +++-- .../edu/kit/typicalc/view/main/InputBar.java | 24 ++++---------- 8 files changed, 54 insertions(+), 41 deletions(-) create mode 100644 frontend/src/input-bar-enhancements.js delete mode 100644 frontend/src/lambda-button-listener.js diff --git a/frontend/src/input-bar-enhancements.js b/frontend/src/input-bar-enhancements.js new file mode 100644 index 0000000..a2ab484 --- /dev/null +++ b/frontend/src/input-bar-enhancements.js @@ -0,0 +1,31 @@ +function changeEvent(element) { + // notify Vaadin + document.getElementById("inputField").__dataValue.value = element.value; + const evt = new Event("change"); + element.dispatchEvent(evt, { 'bubbles': true }); +} + +window.lambdaButtonListener = (buttonID, inputID) => { + document.getElementById(buttonID).addEventListener('click', e => { + const area = document.getElementById(inputID).shadowRoot.querySelector('input'); + let start = area.selectionStart; + area.value = [area.value.slice(0, start), 'λ', area.value.slice(start)].join(''); + area.selectionStart = ++start; + area.selectionEnd = start; + area.focus(); + changeEvent(area); + }); +} +window.backslashListener = (inputID) => { + document.getElementById(inputID).addEventListener('keyup', e => { + const area = e.target.shadowRoot.querySelector('input'); + if (area.value.indexOf('\\') >= 0) { + const start = area.selectionStart; + const end = area.selectionEnd; + area.value = area.value.replaceAll('\\', 'λ'); + area.selectionStart = start; + area.selectionEnd = end; + changeEvent(area); + } + }); +} diff --git a/frontend/src/lambda-button-listener.js b/frontend/src/lambda-button-listener.js deleted file mode 100644 index 5d92df1..0000000 --- a/frontend/src/lambda-button-listener.js +++ /dev/null @@ -1,10 +0,0 @@ -window.lambdaButtonListener = (str1, str2) => { - document.getElementById(str1).addEventListener('click', e => { - var area = document.getElementById(str2).shadowRoot.querySelector('input'); - var start = area.selectionStart; - area.value = [area.value.slice(0, start), 'λ', area.value.slice(start)].join(''); - area.selectionStart = ++start; - area.selectionEnd = start; - area.focus(); - }); -} \ No newline at end of file diff --git a/frontend/src/mathjax-adapter.ts b/frontend/src/mathjax-adapter.ts index d9f734d..8d34c79 100644 --- a/frontend/src/mathjax-adapter.ts +++ b/frontend/src/mathjax-adapter.ts @@ -25,20 +25,16 @@ export abstract class MathjaxAdapter extends LitElement { }); } - connectedCallback() { - super.connectedCallback(); - this.requestTypeset(); - } - render(): TemplateResult { return html`
`; } - protected abstract showStep(n: number): void; + protected showStep(_n: number): void { + /* ignore by default */ + } protected calculateSteps(): void { } } - diff --git a/frontend/src/mathjax-display.ts b/frontend/src/mathjax-display.ts index ff267ab..7107b97 100644 --- a/frontend/src/mathjax-display.ts +++ b/frontend/src/mathjax-display.ts @@ -1,7 +1,10 @@ import {MathjaxAdapter} from "./mathjax-adapter"; class MathjaxDisplay extends MathjaxAdapter { - protected showStep(_n: number): void {} + connectedCallback() { + super.connectedCallback(); + this.requestTypeset(); + } } customElements.define('tc-display', MathjaxDisplay); \ No newline at end of file diff --git a/frontend/src/mathjax-unification.ts b/frontend/src/mathjax-unification.ts index 8f4796f..2a84cb3 100644 --- a/frontend/src/mathjax-unification.ts +++ b/frontend/src/mathjax-unification.ts @@ -1,6 +1,10 @@ import {MathjaxAdapter} from "./mathjax-adapter"; class MathjaxUnification extends MathjaxAdapter { + connectedCallback() { + super.connectedCallback(); + this.requestTypeset(); + } static get properties() { return { @@ -13,4 +17,4 @@ class MathjaxUnification extends MathjaxAdapter { } } -customElements.define('tc-unification', MathjaxUnification); \ No newline at end of file +customElements.define('tc-unification', MathjaxUnification); diff --git a/frontend/styles/view/type-inference.css b/frontend/styles/view/type-inference.css index 7cee23a..94b56a3 100644 --- a/frontend/styles/view/type-inference.css +++ b/frontend/styles/view/type-inference.css @@ -36,7 +36,7 @@ } #rules-button { - height: 6em; + height: 9em; position: fixed; top: 50%; left: 1em; diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java index 2721891..dbcf1f2 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java @@ -26,13 +26,14 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter { /** * Creates a new HTML element that renders the proof tree and cuts it into steps. - * The latex String must consist of exactly one proof tree environment in order for - * this element to work. In other cases the expected behaviour is undefined. + * The latex code must consist of exactly one proof tree environment. + * In other cases unexpected behaviour may occur. * - * @param latex the LaTeX-String to render with MathJax + * @param latex the LaTeX code to render with MathJax */ public MathjaxProofTree(String latex) { content.add(latex); + getElement().callJsFunction("requestTypeset"); } /** 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 5b4b452..560aadd 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -22,7 +22,7 @@ import java.util.function.Consumer; * Contains components which allow the user to enter a lambda term and start the type inference algorithm. */ @CssImport("./styles/view/main/input-bar.css") -@JsModule("./src/lambda-button-listener.js") +@JsModule("./src/input-bar-enhancements.js") public class InputBar extends HorizontalLayout implements LocaleChangeObserver { private static final long serialVersionUID = -6099700300418752958L; @@ -66,17 +66,9 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { inputField.setMaxLength(MAX_INPUT_LENGTH); // attach a listener that replaces \ with λ - // JavaScript is used because Vaadin does not have APIs for selectionStart/selectionEnd - UI.getCurrent().getPage().executeJs( - "document.getElementById('" + INPUT_FIELD_ID + "').addEventListener('keyup', e => {" - + "var area = e.target.shadowRoot.querySelector('input');" - + "if (area.value.indexOf('\\\\') >= 0) {" - + " var start = area.selectionStart;" - + " var end = area.selectionEnd;" - + " area.value = area.value.replaceAll('\\\\', 'λ');" - + " area.selectionStart = start;" - + " area.selectionEnd = end;" - + "}});"); + // JavaScript is used because this is a latency-sensitive operation + // (and Vaadin does not have APIs for selectionStart/selectionEnd) + UI.getCurrent().getPage().executeJs("window.backslashListener($0);", INPUT_FIELD_ID); Button lambdaButton = new Button(getTranslation("root.lambda")); lambdaButton.setId(LAMBDA_BUTTON_ID); UI.getCurrent().getPage().executeJs("window.lambdaButtonListener($0, $1);", LAMBDA_BUTTON_ID, INPUT_FIELD_ID); @@ -118,12 +110,8 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { } private void onTypeInferButtonClick() { - 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())); - }); + inputField.blur(); + callback.accept(Pair.of(inputField.getValue(), typeAssumptionsArea.getTypeAssumptions())); } private void onTypeAssumptionsButton() { From ce01676a4273a81ce90a9ed10d398c33e17c119b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 10 Mar 2021 18:39:41 +0100 Subject: [PATCH 4/5] Convert frontend scripts to TypeScript --- frontend/src/copy-to-clipboard.js | 10 ---- frontend/src/copy-to-clipboard.ts | 11 ++++ frontend/src/input-bar-enhancements.js | 31 ---------- frontend/src/input-bar-enhancements.ts | 38 ++++++++++++ frontend/src/key-shortcuts.js | 30 ---------- frontend/src/key-shortcuts.ts | 30 ++++++++++ frontend/src/mathjax-adapter.ts | 59 ++++++++++--------- frontend/src/mathjax-display.ts | 10 ++-- frontend/src/mathjax-setup.js | 23 ++++---- frontend/src/mathjax-unification.ts | 24 ++++---- frontend/src/share-dialog-autoselect.js | 12 ---- frontend/src/share-dialog-autoselect.ts | 15 +++++ frontend/src/type-input-listener.js | 49 --------------- frontend/src/type-input-listener.ts | 50 ++++++++++++++++ .../typeinferencecontent/ShareDialog.java | 2 +- .../TypeInferenceView.java | 2 +- .../view/main/InferenceRuleField.java | 4 +- .../edu/kit/typicalc/view/main/InputBar.java | 2 +- .../view/main/TypeAssumptionField.java | 12 ++-- tsconfig.json | 1 - 20 files changed, 214 insertions(+), 201 deletions(-) delete mode 100644 frontend/src/copy-to-clipboard.js create mode 100644 frontend/src/copy-to-clipboard.ts delete mode 100644 frontend/src/input-bar-enhancements.js create mode 100644 frontend/src/input-bar-enhancements.ts delete mode 100644 frontend/src/key-shortcuts.js create mode 100644 frontend/src/key-shortcuts.ts delete mode 100644 frontend/src/share-dialog-autoselect.js create mode 100644 frontend/src/share-dialog-autoselect.ts delete mode 100644 frontend/src/type-input-listener.js create mode 100644 frontend/src/type-input-listener.ts diff --git a/frontend/src/copy-to-clipboard.js b/frontend/src/copy-to-clipboard.js deleted file mode 100644 index 921fc18..0000000 --- a/frontend/src/copy-to-clipboard.js +++ /dev/null @@ -1,10 +0,0 @@ -window.copyToClipboard = (str) => { - const textarea = document.createElement("textarea"); - textarea.value = str; - textarea.style.position = "absolute"; - textarea.style.opacity = "0"; - document.body.appendChild(textarea); - textarea.select(); - document.execCommand("copy"); - document.body.removeChild(textarea); -}; \ No newline at end of file diff --git a/frontend/src/copy-to-clipboard.ts b/frontend/src/copy-to-clipboard.ts new file mode 100644 index 0000000..726fd03 --- /dev/null +++ b/frontend/src/copy-to-clipboard.ts @@ -0,0 +1,11 @@ +// @ts-ignore +window.copyToClipboard = (text: string) => { + const textarea = document.createElement("textarea"); + textarea.value = text; + textarea.style.position = "absolute"; + textarea.style.opacity = "0"; + document.body.appendChild(textarea); + textarea.select(); + document.execCommand("copy"); + document.body.removeChild(textarea); +}; diff --git a/frontend/src/input-bar-enhancements.js b/frontend/src/input-bar-enhancements.js deleted file mode 100644 index a2ab484..0000000 --- a/frontend/src/input-bar-enhancements.js +++ /dev/null @@ -1,31 +0,0 @@ -function changeEvent(element) { - // notify Vaadin - document.getElementById("inputField").__dataValue.value = element.value; - const evt = new Event("change"); - element.dispatchEvent(evt, { 'bubbles': true }); -} - -window.lambdaButtonListener = (buttonID, inputID) => { - document.getElementById(buttonID).addEventListener('click', e => { - const area = document.getElementById(inputID).shadowRoot.querySelector('input'); - let start = area.selectionStart; - area.value = [area.value.slice(0, start), 'λ', area.value.slice(start)].join(''); - area.selectionStart = ++start; - area.selectionEnd = start; - area.focus(); - changeEvent(area); - }); -} -window.backslashListener = (inputID) => { - document.getElementById(inputID).addEventListener('keyup', e => { - const area = e.target.shadowRoot.querySelector('input'); - if (area.value.indexOf('\\') >= 0) { - const start = area.selectionStart; - const end = area.selectionEnd; - area.value = area.value.replaceAll('\\', 'λ'); - area.selectionStart = start; - area.selectionEnd = end; - changeEvent(area); - } - }); -} diff --git a/frontend/src/input-bar-enhancements.ts b/frontend/src/input-bar-enhancements.ts new file mode 100644 index 0000000..caf12b5 --- /dev/null +++ b/frontend/src/input-bar-enhancements.ts @@ -0,0 +1,38 @@ +function changeEvent(element: HTMLElement) { + // notify Vaadin + // @ts-ignore + document.getElementById("inputField")!.__dataValue.value = element.value; + const evt = new Event("change", { bubbles: true }); + element.dispatchEvent(evt); +} + +// @ts-ignore +window.lambdaButtonListener = (buttonID: string, inputID: string) => { + const button = document.getElementById(buttonID)!; + const input = document.getElementById(inputID)!; + button.addEventListener('click', () => { + const area = input.shadowRoot!.querySelector('input')!; + let start = area.selectionStart!; + area.value = [area.value.slice(0, start), 'λ', area.value.slice(start)].join(''); + area.selectionStart = ++start; + area.selectionEnd = start; + area.focus(); + changeEvent(area); + }); +} + +// @ts-ignore +window.backslashListener = (inputID: string) => { + document.getElementById(inputID)!.addEventListener('keyup', e => { + const area = (e.target as HTMLElement).shadowRoot!.querySelector('input')!; + if (area.value.indexOf('\\') >= 0) { + const start = area.selectionStart; + const end = area.selectionEnd; + // @ts-ignore + area.value = area.value.replaceAll('\\', 'λ'); + area.selectionStart = start; + area.selectionEnd = end; + changeEvent(area); + } + }); +} diff --git a/frontend/src/key-shortcuts.js b/frontend/src/key-shortcuts.js deleted file mode 100644 index 33b6e86..0000000 --- a/frontend/src/key-shortcuts.js +++ /dev/null @@ -1,30 +0,0 @@ -document.onkeydown = handleKey; - -function handleKey(e) { - if (e.target.tagName.toLowerCase() === "vaadin-text-field") { - return; - } - let element = null; - if (e.keyCode === 37) { - // left arrow - if (!e.ctrlKey) { - element = document.getElementById("previous-step"); - } else { - element = document.getElementById("first-step"); - } - } else if (e.keyCode === 39) { - // right arrow - if (!e.ctrlKey) { - element = document.getElementById("next-step"); - } else { - element = document.getElementById("last-step"); - } - } else if (e.key === "/") { - document.getElementById("inputField").focus(); - e.preventDefault(); - } - if (element !== null) { - element.click(); - e.preventDefault(); - } -} diff --git a/frontend/src/key-shortcuts.ts b/frontend/src/key-shortcuts.ts new file mode 100644 index 0000000..e002d9b --- /dev/null +++ b/frontend/src/key-shortcuts.ts @@ -0,0 +1,30 @@ +document.onkeydown = handleKey; + +function handleKey(e: KeyboardEvent) { + if ((e.target! as HTMLElement).tagName.toLowerCase() === "vaadin-text-field") { + return; + } + let element = null; + if (e.code === "ArrowLeft") { + // left arrow + if (!e.ctrlKey) { + element = document.getElementById("previous-step"); + } else { + element = document.getElementById("first-step"); + } + } else if (e.code === "ArrowRight") { + // right arrow + if (!e.ctrlKey) { + element = document.getElementById("next-step"); + } else { + element = document.getElementById("last-step"); + } + } else if (e.key === "/") { + document.getElementById("inputField")!.focus(); + e.preventDefault(); + } + if (element !== null) { + element.click(); + e.preventDefault(); + } +} diff --git a/frontend/src/mathjax-adapter.ts b/frontend/src/mathjax-adapter.ts index 8d34c79..08ee367 100644 --- a/frontend/src/mathjax-adapter.ts +++ b/frontend/src/mathjax-adapter.ts @@ -1,40 +1,41 @@ import {LitElement, html} from 'lit-element'; import {TemplateResult} from "lit-html"; + declare let window: { - MathJax: { - typesetShadow: (shadowRoot: ShadowRoot, callback: () => void) => void, - isInitialized: boolean, - }; - addEventListener: (event: string, listener: () => void) => void; + MathJax: { + typesetShadow: (shadowRoot: ShadowRoot, callback: () => void) => void, + isInitialized: boolean, + }; + addEventListener: (event: string, listener: () => void) => void; }; export abstract class MathjaxAdapter extends LitElement { - private execTypeset(shadowRoot: ShadowRoot) { - if (window.MathJax) { - window.MathJax.typesetShadow(shadowRoot, () => this.calculateSteps()); - } - } + private execTypeset(shadowRoot: ShadowRoot) { + if (window.MathJax) { + window.MathJax.typesetShadow(shadowRoot, () => this.calculateSteps()); + } + } - protected requestTypeset() { - this.updateComplete.then(() => { - if (window.MathJax === undefined || !window.MathJax.isInitialized) { - window.addEventListener('mathjax-initialized', () => this.execTypeset(this.shadowRoot!)); - } else { - this.execTypeset(this.shadowRoot!); - } - }); - } + protected requestTypeset() { + this.updateComplete.then(() => { + if (window.MathJax === undefined || !window.MathJax.isInitialized) { + window.addEventListener('mathjax-initialized', () => this.execTypeset(this.shadowRoot!)); + } else { + this.execTypeset(this.shadowRoot!); + } + }); + } - render(): TemplateResult { - return html` -
- `; - } + render(): TemplateResult { + return html` +
+ `; + } - protected showStep(_n: number): void { - /* ignore by default */ - } + protected showStep(_n: number): void { + /* ignore by default */ + } - protected calculateSteps(): void { - } + protected calculateSteps(): void { + } } diff --git a/frontend/src/mathjax-display.ts b/frontend/src/mathjax-display.ts index 7107b97..e866ff9 100644 --- a/frontend/src/mathjax-display.ts +++ b/frontend/src/mathjax-display.ts @@ -1,10 +1,10 @@ import {MathjaxAdapter} from "./mathjax-adapter"; class MathjaxDisplay extends MathjaxAdapter { - connectedCallback() { - super.connectedCallback(); - this.requestTypeset(); - } + connectedCallback() { + super.connectedCallback(); + this.requestTypeset(); + } } -customElements.define('tc-display', MathjaxDisplay); \ No newline at end of file +customElements.define('tc-display', MathjaxDisplay); diff --git a/frontend/src/mathjax-setup.js b/frontend/src/mathjax-setup.js index e1e14cc..63547ed 100644 --- a/frontend/src/mathjax-setup.js +++ b/frontend/src/mathjax-setup.js @@ -4,7 +4,9 @@ SVGElement.prototype.getTransformToElement = SVGElement.prototype.getTransformTo return elem.getScreenCTM().inverse().multiply(this.getScreenCTM()); }; window.MathJax = { - loader: {load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/color', '[tex]/textmacros', '[tex]/unicode']}, + loader: { + load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/color', '[tex]/textmacros', '[tex]/unicode'] + }, tex: { packages: {'[+]': ['ams', 'bussproofs', 'color', 'textmacros', 'unicode']}, inlineMath: [['$', '$'], ['\\(', '\\)']] @@ -86,7 +88,7 @@ window.MathJax = { // you need to rerender the shadowRoot later. // MathJax.typesetShadow = function (root, callback) { - if (root.getElementById("tc-content") == null) { + if (root.getElementById("tc-content") === null) { return; } const mjxContainer = root.querySelector("mjx-container"); @@ -104,17 +106,16 @@ window.MathJax = { } return html; } - if (root.querySelector("#style-fixes") == null) { + // set the size of the rendered SVG to the size of the container element + if (root.querySelector("#style-fixes") === null) { const style = document.createElement('style'); - style.type = "text/css"; style.innerHTML = "\ -mjx-doc, mjx-body, mjx-container, #tc-content, svg {\ - height: 100%;\ -}\ -mjx-container {\ - margin: 0 !important;\ -}\ - "; + mjx-doc, mjx-body, mjx-container, #tc-content, svg {\ + height: 100%;\ + }\ + mjx-container {\ + margin: 0 !important;\ + }"; if (hostTag === "tc-proof-tree") { style.innerHTML += "svg { width: 100%; }"; } diff --git a/frontend/src/mathjax-unification.ts b/frontend/src/mathjax-unification.ts index 2a84cb3..19857a5 100644 --- a/frontend/src/mathjax-unification.ts +++ b/frontend/src/mathjax-unification.ts @@ -1,20 +1,20 @@ import {MathjaxAdapter} from "./mathjax-adapter"; class MathjaxUnification extends MathjaxAdapter { - connectedCallback() { - super.connectedCallback(); - this.requestTypeset(); - } + connectedCallback() { + super.connectedCallback(); + this.requestTypeset(); + } - static get properties() { - return { - content: {type: String} - } - } + static get properties() { + return { + content: {type: String} + } + } - protected showStep(_n: number): void { - this.requestTypeset(); - } + protected showStep(_n: number): void { + this.requestTypeset(); + } } customElements.define('tc-unification', MathjaxUnification); diff --git a/frontend/src/share-dialog-autoselect.js b/frontend/src/share-dialog-autoselect.js deleted file mode 100644 index 05c3f26..0000000 --- a/frontend/src/share-dialog-autoselect.js +++ /dev/null @@ -1,12 +0,0 @@ -window.autoSelect = (className) => { - let el = document.getElementsByClassName(className); - Array.from(el).forEach(field => { - field.addEventListener('focus', event => { - let e = event.target.shadowRoot.querySelector('input'); - if (!e) { - e = event.target.shadowRoot.querySelector('textArea'); - } - e.setSelectionRange(0, e.value.length); - }); - }); -} \ No newline at end of file diff --git a/frontend/src/share-dialog-autoselect.ts b/frontend/src/share-dialog-autoselect.ts new file mode 100644 index 0000000..36bc849 --- /dev/null +++ b/frontend/src/share-dialog-autoselect.ts @@ -0,0 +1,15 @@ +// @ts-ignore +window.autoSelect = (className: string) => { + let el = document.getElementsByClassName(className); + Array.from(el).forEach(field => { + field.addEventListener('focus', event => { + const root = (event.target! as HTMLElement).shadowRoot!; + let e: HTMLInputElement | HTMLTextAreaElement | null + = root.querySelector('input'); + if (!e) { + e = root.querySelector('textArea')!; + } + e.setSelectionRange(0, e.value.length); + }); + }); +} diff --git a/frontend/src/type-input-listener.js b/frontend/src/type-input-listener.js deleted file mode 100644 index 479aadf..0000000 --- a/frontend/src/type-input-listener.js +++ /dev/null @@ -1,49 +0,0 @@ -const subscripted = [...'\u2080\u2081\u2082\u2083\u2084\u2085\u2086\u2087\u2088\u2089']; - -window.addTypeInputListener = (str) => { - var el = document.getElementsByClassName(str); - if (el) { - Array.from(el).forEach(function(element) { - element.addEventListener('keyup', e => { - var area = e.target.shadowRoot.querySelector('input'); - listener(area); - }); - }); - Array.from(el).forEach(function(element) { - element.addEventListener('focus', e => { - var area = e.target.shadowRoot.querySelector('input'); - listener(area); - }); - }); - } -} - -function listener(area) { - var value = parseBack(area.value); - var start = area.selectionStart; - var end = area.selectionEnd; - // ignore brackets, allow '>' or spaces in front and '-' or spaces at the end of string - area.value = value.replace(/(^|\s+|\(|\)|>)t[0-9]+(?=\s+|\)|\(|\-|$)/ig, replacer); - area.selectionStart = start; - area.selectionEnd = end; -} - -function replacer(value) { - value = value.replace('t', '\u03C4'); - return value.replace(/[0123456789]/g, toUnicode); -} - -function toUnicode(number) { - return subscripted[number]; -} - -function toNumber(unicode) { - var result = subscripted.indexOf(unicode); - if(result > -1) { return result; } - else { return unicode; } -} - -function parseBack(value) { - value = value.replaceAll('\u03C4', 't'); - return value.replace(/./g, toNumber); -} \ No newline at end of file diff --git a/frontend/src/type-input-listener.ts b/frontend/src/type-input-listener.ts new file mode 100644 index 0000000..a904138 --- /dev/null +++ b/frontend/src/type-input-listener.ts @@ -0,0 +1,50 @@ +const subscripted = [...'\u2080\u2081\u2082\u2083\u2084\u2085\u2086\u2087\u2088\u2089']; + +// @ts-ignore +window.addTypeInputListener = (className: string) => { + const el = document.getElementsByClassName(className); + if (el) { + const listener = (e: Event) => { + const area = (e.target! as HTMLElement).shadowRoot!.querySelector('input'); + modifyValue(area!); + }; + Array.from(el).forEach(function (element) { + element.addEventListener('keyup', listener); + element.addEventListener('focus', listener); + }); + } +} + +function modifyValue(area: HTMLInputElement) { + const value = parseBack(area.value); + const start = area.selectionStart; + const end = area.selectionEnd; + // ignore brackets, allow '>' or spaces in front and '-' or spaces at the end of string + area.value = value.replace(/(^|\s+|\(|\)|>)t[0-9]+(?=\s+|\)|\(|-|$)/ig, replacer); + area.selectionStart = start; + area.selectionEnd = end; +} + +function replacer(value: string) { + value = value.replace('t', '\u03C4'); + return value.replace(/[0123456789]/g, toUnicode); +} + +function toUnicode(number: string, ..._args: any[]) { + return subscripted[Number(number)]; +} + +function toNumber(unicode: string, ..._args: any[]) { + const result = subscripted.indexOf(unicode); + if (result > -1) { + return result.toString(); + } else { + return unicode; + } +} + +function parseBack(value: string) { + // @ts-ignore + value = value.replaceAll('\u03C4', 't'); + return value.replace(/./g, toNumber); +} diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java index 6ba350f..b7808a4 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java @@ -17,7 +17,7 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; /** * Contains GUI elements to extract the URL and LaTeX code of the currently shown proof tree. */ -@JsModule("./src/share-dialog-autoselect.js") +@JsModule("./src/share-dialog-autoselect.ts") @CssImport("./styles/view/share-dialog.css") public class ShareDialog extends Dialog implements LocaleChangeObserver { 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 167e096..8cd53c3 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 @@ -35,7 +35,7 @@ import java.util.Locale; * {@link TypeInfererInterface} and MathJax to render the LaTeX to the user. */ @CssImport("./styles/view/type-inference.css") -@JavaScript("./src/key-shortcuts.js") +@JavaScript("./src/key-shortcuts.ts") @Route(value = TypeInferenceView.ROUTE + "/:term", layout = MainViewImpl.class) public class TypeInferenceView extends VerticalLayout implements ControlPanelView, ComponentEventListener, LocaleChangeObserver, HasDynamicTitle, diff --git a/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java b/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java index 93674c7..19f9816 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java +++ b/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java @@ -20,7 +20,7 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; * clipboard. Each InferenceRuleField is displayed in drawer area of the web page. */ @CssImport("./styles/view/main/inference-rule-field.css") -@JsModule("./src/copy-to-clipboard.js") +@JsModule("./src/copy-to-clipboard.ts") public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver { private static final long serialVersionUID = -8551851183297707985L; @@ -67,7 +67,7 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb add(header, main); setId(INFERENCE_RULE_FIELD_ID); } - + @Override public void localeChange(LocaleChangeEvent event) { ruleName.setText(getTranslation(nameKey)); 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 560aadd..f7f26ed 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -22,7 +22,7 @@ import java.util.function.Consumer; * Contains components which allow the user to enter a lambda term and start the type inference algorithm. */ @CssImport("./styles/view/main/input-bar.css") -@JsModule("./src/input-bar-enhancements.js") +@JsModule("./src/input-bar-enhancements.ts") public class InputBar extends HorizontalLayout implements LocaleChangeObserver { private static final long serialVersionUID = -6099700300418752958L; 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 1391656..d93587d 100644 --- a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java +++ b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java @@ -21,7 +21,7 @@ import java.util.function.Consumer; * Represents a single type assumption input component. * Each TypeAssumptionField is displayed in the TypeAssumptionsArea. */ -@JsModule("./src/type-input-listener.js") +@JsModule("./src/type-input-listener.ts") @CssImport("./styles/view/main/type-assumption-field.css") @CssImport(value = "./styles/view/main/type-assumption-input-field.css", themeFor = "vaadin-text-field") public class TypeAssumptionField extends HorizontalLayout implements LocaleChangeObserver { @@ -85,27 +85,27 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang 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) diff --git a/tsconfig.json b/tsconfig.json index 586ec18..280cf89 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -10,7 +10,6 @@ "noImplicitReturns": true, "noImplicitAny": true, "noImplicitThis": true, - "noUnusedLocals": true, "noUnusedParameters": true, "experimentalDecorators": true }, From 47aa0066556ebb373c34ec515837bf560dca0be6 Mon Sep 17 00:00:00 2001 From: Johanna Stuber Date: Wed, 10 Mar 2021 19:38:51 +0100 Subject: [PATCH 5/5] highlight new constraints in unification --- .../latexcreator/LatexCreatorConstants.java | 2 +- .../latexcreator/LatexCreatorConstraints.java | 29 +++++++++++++------ 2 files changed, 21 insertions(+), 10 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java index 0a1e65c..e695a17 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java @@ -54,7 +54,7 @@ public final class LatexCreatorConstants { protected static final String CIRC = "\\circ"; protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}"; protected static final String COLOR_RED = "\\color{#f00}"; - protected static final String COLOR_HIGHLIGHT = "\\color{#b0b}"; + protected static final String COLOR_HIGHLIGHT = "\\color{#006AF5}"; protected static final String EMPTY_SET = "\\emptyset"; protected static final String LAMBDA = "\\lambda"; protected static final String LATEX_SPACE = "\\ "; diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java index aae2285..ab6e30f 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java @@ -259,7 +259,8 @@ public class LatexCreatorConstraints implements StepVisitor { .orElseThrow(IllegalStateException::new); // store constraints of previous step to highlight changes String[] previousConstraints = new String[0]; - for (UnificationStep step : unificationSteps) { + for (int stepNum = 0; stepNum < unificationSteps.size(); stepNum++) { + UnificationStep step = unificationSteps.get(stepNum); List constraints2 = new ArrayList<>(); Result, UnificationError> subs = step.getSubstitutions(); Optional error = Optional.empty(); @@ -276,6 +277,9 @@ public class LatexCreatorConstraints implements StepVisitor { boolean markError = error.isPresent(); List unificationConstraints = step.getConstraints(); + // if new constraints were created in this step, mark them + boolean markLastTwoConstraints = (stepNum != 0) + && unificationSteps.get(stepNum - 1).getConstraints().size() < unificationConstraints.size(); if (!unificationConstraints.isEmpty()) { latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT); } @@ -285,11 +289,14 @@ public class LatexCreatorConstraints implements StepVisitor { if (markError && i == 0) { sb.append(CURLY_LEFT); sb.append(COLOR_RED); + } else if (markLastTwoConstraints && (i < 2)) { + sb.append(CURLY_LEFT); + sb.append(COLOR_HIGHLIGHT); } sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex()); sb.append(EQUALS); sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex()); - if (markError && i == 0) { + if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) { sb.append(CURLY_RIGHT); } constraints2.add(sb.toString()); @@ -299,13 +306,17 @@ public class LatexCreatorConstraints implements StepVisitor { // perform the substitution "manually" and color the new type Substitution s = substitutions.get(substitutions.size() - 1); String original = previousConstraints[invIdx]; - StringBuilder highlightedChange2 = new StringBuilder(); - highlightedChange2.append(CURLY_LEFT); - highlightedChange2.append(COLOR_HIGHLIGHT); - highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex()); - highlightedChange2.append(CURLY_RIGHT); - latex.append(original.replace(new LatexCreatorType(s.getVariable()).getLatex(), - highlightedChange2.toString())); + String originalType = new LatexCreatorType(s.getVariable()).getLatex(); + if (original.contains(originalType)) { + StringBuilder highlightedChange2 = new StringBuilder(); + highlightedChange2.append(CURLY_LEFT); + highlightedChange2.append(COLOR_HIGHLIGHT); + highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex()); + highlightedChange2.append(CURLY_RIGHT); + latex.append(original.replace(originalType, highlightedChange2.toString())); + } else { + latex.append(sb.toString()); + } } else { latex.append(sb.toString()); }