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.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/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..08ee367 100644 --- a/frontend/src/mathjax-adapter.ts +++ b/frontend/src/mathjax-adapter.ts @@ -1,44 +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!); + } + }); + } - connectedCallback() { - super.connectedCallback(); - this.requestTypeset(); - } + render(): TemplateResult { + return html` +
+ `; + } - render(): TemplateResult { - return html` -
- `; - } + protected showStep(_n: number): void { + /* ignore by default */ + } - protected abstract showStep(n: number): void; - - protected calculateSteps(): void { - } + protected calculateSteps(): void { + } } - diff --git a/frontend/src/mathjax-display.ts b/frontend/src/mathjax-display.ts index ff267ab..e866ff9 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 +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 8f4796f..19857a5 100644 --- a/frontend/src/mathjax-unification.ts +++ b/frontend/src/mathjax-unification.ts @@ -1,16 +1,20 @@ import {MathjaxAdapter} from "./mathjax-adapter"; class MathjaxUnification extends MathjaxAdapter { + 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); \ No newline at end of file +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/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/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 @@ - + , 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 5b4b452..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/lambda-button-listener.js") +@JsModule("./src/input-bar-enhancements.ts") 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() { 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 },