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,
@@ -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();
}
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());
}
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 8033a43..6c3b453 100644
--- a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java
+++ b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java
@@ -22,7 +22,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 {
@@ -92,27 +92,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 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 parser.parseType(parseBackType(type)).isOk();
}
-
+
private void addValidatior() {
varBinder.forField(variableInputField)
.withValidator(var -> (hasCorrectVariable(var) || isEmpty()), StringUtils.EMPTY)
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
},