Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

frontend/src/copy-to-clipboard.js

@@ -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);
-};

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);
+};

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);
+		}
+	});
+}

frontend/src/key-shortcuts.js

@@ -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();
-    }
-}

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();
+	}
+}

frontend/src/lambda-button-listener.js

@@ -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();
-	});
-}

frontend/src/mathjax-adapter.ts

@@ -1,5 +1,6 @@
 import {LitElement, html} from 'lit-element';
 import {TemplateResult} from "lit-html";
+
 declare let window: {
 	MathJax: {
 		typesetShadow: (shadowRoot: ShadowRoot, callback: () => void) => void,
@@ -25,20 +26,16 @@ export abstract class MathjaxAdapter extends LitElement {
 		});
 	}
 
-    connectedCallback() {
-        super.connectedCallback();
-        this.requestTypeset();
-    }
-
 	render(): TemplateResult {
 		return html`<mjx-doc id="mjx-document"><mjx-head></mjx-head><mjx-body>
 			<div id="tc-content"></div>
 		</mjx-body></mjx-doc>`;
 	}
 
-    protected abstract showStep(n: number): void;
+	protected showStep(_n: number): void {
+		/* ignore by default */
+	}
 
 	protected calculateSteps(): void {
 	}
 }
-

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);

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<HTMLElement>("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 {\
+                        mjx-doc, mjx-body, mjx-container, #tc-content, svg {\
                             height: 100%;\
-}\
-mjx-container {\
+                        }\
+                        mjx-container {\
                             margin: 0 !important;\
-}\
-                    ";
+                        }";
                     if (hostTag === "tc-proof-tree") {
                         style.innerHTML += "svg { width: 100%; }";
                     }

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 {

frontend/src/share-dialog-autoselect.js

@@ -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);
-		});
-	});
-}

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<HTMLInputElement>('input');
+			if (!e) {
+				e = root.querySelector<HTMLTextAreaElement>('textArea')!;
+			}
+			e.setSelectionRange(0, e.value.length);
+		});
+	});
+}

frontend/src/type-input-listener.js

@@ -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);
-}

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<HTMLInputElement>('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);
+}

frontend/styles/view/type-inference.css

@@ -36,7 +36,7 @@
 }
 
 #rules-button {
-	height: 6em;
+	height: 9em;
 	position: fixed;
 	top: 50%;
 	left: 1em;

pom.xml

@@ -1,5 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
     <modelVersion>4.0.0</modelVersion>
     <groupId>edu.kit.typicalc</groupId>
     <artifactId>typicalc</artifactId>
@@ -280,10 +282,12 @@
                                 <mkdir dir="${project.build.directory}/tmp" />
                                 <unzip src="${project.build.directory}/${project.build.finalName}.jar"
                                        dest="${project.build.directory}/tmp" />
-                                <replaceregexp file="${project.build.directory}/tmp/META-INF/VAADIN/index.html"
+                                <replaceregexp file="${project.build.directory}/tmp/META-INF/VAADIN/webapp/index.html"
                                                match="(\x3C)body(\x3E)"
                                                replace="\1body\2 \1noscript\2This application requires JavaScript.\1/noscript\2"
                                                byline="true" />
+                                <gzip src="${project.build.directory}/tmp/META-INF/VAADIN/webapp/index.html"
+                                      destfile="${project.build.directory}/tmp/META-INF/VAADIN/webapp/index.html.gz" />
                                 <zip basedir="${project.build.directory}/tmp"
                                      destfile="${project.build.directory}/${project.build.finalName}.jar"
                                      update="true"

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");
     }
 
     /**

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 {
 

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<AttachEvent>, LocaleChangeObserver, HasDynamicTitle,

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;

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()));
-            });
+        callback.accept(Pair.of(inputField.getValue(), typeAssumptionsArea.getTypeAssumptions()));
     }
 
     private void onTypeAssumptionsButton() {

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 {

tsconfig.json

@@ -10,7 +10,6 @@
     "noImplicitReturns": true,
     "noImplicitAny": true,
     "noImplicitThis": true,
-    "noUnusedLocals": true,
     "noUnusedParameters": true,
     "experimentalDecorators": true
   },