mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
1f1db955d3
@ -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);
|
|
||||||
};
|
|
11
frontend/src/copy-to-clipboard.ts
Normal file
11
frontend/src/copy-to-clipboard.ts
Normal file
@ -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);
|
||||||
|
};
|
38
frontend/src/input-bar-enhancements.ts
Normal file
38
frontend/src/input-bar-enhancements.ts
Normal file
@ -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);
|
||||||
|
}
|
||||||
|
});
|
||||||
|
}
|
@ -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();
|
|
||||||
}
|
|
||||||
}
|
|
30
frontend/src/key-shortcuts.ts
Normal file
30
frontend/src/key-shortcuts.ts
Normal file
@ -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();
|
||||||
|
}
|
||||||
|
}
|
@ -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();
|
|
||||||
});
|
|
||||||
}
|
|
@ -1,5 +1,6 @@
|
|||||||
import {LitElement, html} from 'lit-element';
|
import {LitElement, html} from 'lit-element';
|
||||||
import {TemplateResult} from "lit-html";
|
import {TemplateResult} from "lit-html";
|
||||||
|
|
||||||
declare let window: {
|
declare let window: {
|
||||||
MathJax: {
|
MathJax: {
|
||||||
typesetShadow: (shadowRoot: ShadowRoot, callback: () => void) => void,
|
typesetShadow: (shadowRoot: ShadowRoot, callback: () => void) => void,
|
||||||
@ -25,20 +26,16 @@ export abstract class MathjaxAdapter extends LitElement {
|
|||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
connectedCallback() {
|
|
||||||
super.connectedCallback();
|
|
||||||
this.requestTypeset();
|
|
||||||
}
|
|
||||||
|
|
||||||
render(): TemplateResult {
|
render(): TemplateResult {
|
||||||
return html`<mjx-doc id="mjx-document"><mjx-head></mjx-head><mjx-body>
|
return html`<mjx-doc id="mjx-document"><mjx-head></mjx-head><mjx-body>
|
||||||
<div id="tc-content"></div>
|
<div id="tc-content"></div>
|
||||||
</mjx-body></mjx-doc>`;
|
</mjx-body></mjx-doc>`;
|
||||||
}
|
}
|
||||||
|
|
||||||
protected abstract showStep(n: number): void;
|
protected showStep(_n: number): void {
|
||||||
|
/* ignore by default */
|
||||||
|
}
|
||||||
|
|
||||||
protected calculateSteps(): void {
|
protected calculateSteps(): void {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,7 +1,10 @@
|
|||||||
import {MathjaxAdapter} from "./mathjax-adapter";
|
import {MathjaxAdapter} from "./mathjax-adapter";
|
||||||
|
|
||||||
class MathjaxDisplay extends MathjaxAdapter {
|
class MathjaxDisplay extends MathjaxAdapter {
|
||||||
protected showStep(_n: number): void {}
|
connectedCallback() {
|
||||||
|
super.connectedCallback();
|
||||||
|
this.requestTypeset();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
customElements.define('tc-display', MathjaxDisplay);
|
customElements.define('tc-display', MathjaxDisplay);
|
@ -4,7 +4,9 @@ SVGElement.prototype.getTransformToElement = SVGElement.prototype.getTransformTo
|
|||||||
return elem.getScreenCTM().inverse().multiply(this.getScreenCTM());
|
return elem.getScreenCTM().inverse().multiply(this.getScreenCTM());
|
||||||
};
|
};
|
||||||
window.MathJax = {
|
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: {
|
tex: {
|
||||||
packages: {'[+]': ['ams', 'bussproofs', 'color', 'textmacros', 'unicode']},
|
packages: {'[+]': ['ams', 'bussproofs', 'color', 'textmacros', 'unicode']},
|
||||||
inlineMath: [['$', '$'], ['\\(', '\\)']]
|
inlineMath: [['$', '$'], ['\\(', '\\)']]
|
||||||
@ -86,7 +88,7 @@ window.MathJax = {
|
|||||||
// you need to rerender the shadowRoot later.
|
// you need to rerender the shadowRoot later.
|
||||||
//
|
//
|
||||||
MathJax.typesetShadow = function (root, callback) {
|
MathJax.typesetShadow = function (root, callback) {
|
||||||
if (root.getElementById("tc-content") == null) {
|
if (root.getElementById("tc-content") === null) {
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
const mjxContainer = root.querySelector<HTMLElement>("mjx-container");
|
const mjxContainer = root.querySelector<HTMLElement>("mjx-container");
|
||||||
@ -104,17 +106,16 @@ window.MathJax = {
|
|||||||
}
|
}
|
||||||
return html;
|
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');
|
const style = document.createElement('style');
|
||||||
style.type = "text/css";
|
|
||||||
style.innerHTML = "\
|
style.innerHTML = "\
|
||||||
mjx-doc, mjx-body, mjx-container, #tc-content, svg {\
|
mjx-doc, mjx-body, mjx-container, #tc-content, svg {\
|
||||||
height: 100%;\
|
height: 100%;\
|
||||||
}\
|
}\
|
||||||
mjx-container {\
|
mjx-container {\
|
||||||
margin: 0 !important;\
|
margin: 0 !important;\
|
||||||
}\
|
}";
|
||||||
";
|
|
||||||
if (hostTag === "tc-proof-tree") {
|
if (hostTag === "tc-proof-tree") {
|
||||||
style.innerHTML += "svg { width: 100%; }";
|
style.innerHTML += "svg { width: 100%; }";
|
||||||
}
|
}
|
||||||
|
@ -1,6 +1,10 @@
|
|||||||
import {MathjaxAdapter} from "./mathjax-adapter";
|
import {MathjaxAdapter} from "./mathjax-adapter";
|
||||||
|
|
||||||
class MathjaxUnification extends MathjaxAdapter {
|
class MathjaxUnification extends MathjaxAdapter {
|
||||||
|
connectedCallback() {
|
||||||
|
super.connectedCallback();
|
||||||
|
this.requestTypeset();
|
||||||
|
}
|
||||||
|
|
||||||
static get properties() {
|
static get properties() {
|
||||||
return {
|
return {
|
||||||
|
@ -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);
|
|
||||||
});
|
|
||||||
});
|
|
||||||
}
|
|
15
frontend/src/share-dialog-autoselect.ts
Normal file
15
frontend/src/share-dialog-autoselect.ts
Normal file
@ -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);
|
||||||
|
});
|
||||||
|
});
|
||||||
|
}
|
@ -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);
|
|
||||||
}
|
|
50
frontend/src/type-input-listener.ts
Normal file
50
frontend/src/type-input-listener.ts
Normal file
@ -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);
|
||||||
|
}
|
@ -36,7 +36,7 @@
|
|||||||
}
|
}
|
||||||
|
|
||||||
#rules-button {
|
#rules-button {
|
||||||
height: 6em;
|
height: 9em;
|
||||||
position: fixed;
|
position: fixed;
|
||||||
top: 50%;
|
top: 50%;
|
||||||
left: 1em;
|
left: 1em;
|
||||||
|
8
pom.xml
8
pom.xml
@ -1,5 +1,7 @@
|
|||||||
<?xml version="1.0" encoding="UTF-8"?>
|
<?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>
|
<modelVersion>4.0.0</modelVersion>
|
||||||
<groupId>edu.kit.typicalc</groupId>
|
<groupId>edu.kit.typicalc</groupId>
|
||||||
<artifactId>typicalc</artifactId>
|
<artifactId>typicalc</artifactId>
|
||||||
@ -280,10 +282,12 @@
|
|||||||
<mkdir dir="${project.build.directory}/tmp" />
|
<mkdir dir="${project.build.directory}/tmp" />
|
||||||
<unzip src="${project.build.directory}/${project.build.finalName}.jar"
|
<unzip src="${project.build.directory}/${project.build.finalName}.jar"
|
||||||
dest="${project.build.directory}/tmp" />
|
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)"
|
match="(\x3C)body(\x3E)"
|
||||||
replace="\1body\2 \1noscript\2This application requires JavaScript.\1/noscript\2"
|
replace="\1body\2 \1noscript\2This application requires JavaScript.\1/noscript\2"
|
||||||
byline="true" />
|
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"
|
<zip basedir="${project.build.directory}/tmp"
|
||||||
destfile="${project.build.directory}/${project.build.finalName}.jar"
|
destfile="${project.build.directory}/${project.build.finalName}.jar"
|
||||||
update="true"
|
update="true"
|
||||||
|
@ -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.
|
* 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
|
* The latex code must consist of exactly one proof tree environment.
|
||||||
* this element to work. In other cases the expected behaviour is undefined.
|
* 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) {
|
public MathjaxProofTree(String latex) {
|
||||||
content.add(latex);
|
content.add(latex);
|
||||||
|
getElement().callJsFunction("requestTypeset");
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -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.
|
* 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")
|
@CssImport("./styles/view/share-dialog.css")
|
||||||
public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
||||||
|
|
||||||
|
@ -35,7 +35,7 @@ import java.util.Locale;
|
|||||||
* {@link TypeInfererInterface} and MathJax to render the LaTeX to the user.
|
* {@link TypeInfererInterface} and MathJax to render the LaTeX to the user.
|
||||||
*/
|
*/
|
||||||
@CssImport("./styles/view/type-inference.css")
|
@CssImport("./styles/view/type-inference.css")
|
||||||
@JavaScript("./src/key-shortcuts.js")
|
@JavaScript("./src/key-shortcuts.ts")
|
||||||
@Route(value = TypeInferenceView.ROUTE + "/:term", layout = MainViewImpl.class)
|
@Route(value = TypeInferenceView.ROUTE + "/:term", layout = MainViewImpl.class)
|
||||||
public class TypeInferenceView extends VerticalLayout
|
public class TypeInferenceView extends VerticalLayout
|
||||||
implements ControlPanelView, ComponentEventListener<AttachEvent>, LocaleChangeObserver, HasDynamicTitle,
|
implements ControlPanelView, ComponentEventListener<AttachEvent>, LocaleChangeObserver, HasDynamicTitle,
|
||||||
@ -185,6 +185,7 @@ public class TypeInferenceView extends VerticalLayout
|
|||||||
content.removeAll();
|
content.removeAll();
|
||||||
lc = new LatexCreator(typeInferer,
|
lc = new LatexCreator(typeInferer,
|
||||||
error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)));
|
error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)));
|
||||||
|
treeNumbers = lc.getTreeNumbers();
|
||||||
setContent();
|
setContent();
|
||||||
refreshElements();
|
refreshElements();
|
||||||
}
|
}
|
||||||
|
@ -54,7 +54,7 @@ public final class LatexCreatorConstants {
|
|||||||
protected static final String CIRC = "\\circ";
|
protected static final String CIRC = "\\circ";
|
||||||
protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}";
|
protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}";
|
||||||
protected static final String COLOR_RED = "\\color{#f00}";
|
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 EMPTY_SET = "\\emptyset";
|
||||||
protected static final String LAMBDA = "\\lambda";
|
protected static final String LAMBDA = "\\lambda";
|
||||||
protected static final String LATEX_SPACE = "\\ ";
|
protected static final String LATEX_SPACE = "\\ ";
|
||||||
|
@ -259,7 +259,8 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
.orElseThrow(IllegalStateException::new);
|
.orElseThrow(IllegalStateException::new);
|
||||||
// store constraints of previous step to highlight changes
|
// store constraints of previous step to highlight changes
|
||||||
String[] previousConstraints = new String[0];
|
String[] previousConstraints = new String[0];
|
||||||
for (UnificationStep step : unificationSteps) {
|
for (int stepNum = 0; stepNum < unificationSteps.size(); stepNum++) {
|
||||||
|
UnificationStep step = unificationSteps.get(stepNum);
|
||||||
List<String> constraints2 = new ArrayList<>();
|
List<String> constraints2 = new ArrayList<>();
|
||||||
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
|
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
|
||||||
Optional<UnificationError> error = Optional.empty();
|
Optional<UnificationError> error = Optional.empty();
|
||||||
@ -276,6 +277,9 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
|
|
||||||
boolean markError = error.isPresent();
|
boolean markError = error.isPresent();
|
||||||
List<Constraint> unificationConstraints = step.getConstraints();
|
List<Constraint> 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()) {
|
if (!unificationConstraints.isEmpty()) {
|
||||||
latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT);
|
latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT);
|
||||||
}
|
}
|
||||||
@ -285,11 +289,14 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
if (markError && i == 0) {
|
if (markError && i == 0) {
|
||||||
sb.append(CURLY_LEFT);
|
sb.append(CURLY_LEFT);
|
||||||
sb.append(COLOR_RED);
|
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(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex());
|
||||||
sb.append(EQUALS);
|
sb.append(EQUALS);
|
||||||
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex());
|
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex());
|
||||||
if (markError && i == 0) {
|
if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) {
|
||||||
sb.append(CURLY_RIGHT);
|
sb.append(CURLY_RIGHT);
|
||||||
}
|
}
|
||||||
constraints2.add(sb.toString());
|
constraints2.add(sb.toString());
|
||||||
@ -299,13 +306,17 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
// perform the substitution "manually" and color the new type
|
// perform the substitution "manually" and color the new type
|
||||||
Substitution s = substitutions.get(substitutions.size() - 1);
|
Substitution s = substitutions.get(substitutions.size() - 1);
|
||||||
String original = previousConstraints[invIdx];
|
String original = previousConstraints[invIdx];
|
||||||
|
String originalType = new LatexCreatorType(s.getVariable()).getLatex();
|
||||||
|
if (original.contains(originalType)) {
|
||||||
StringBuilder highlightedChange2 = new StringBuilder();
|
StringBuilder highlightedChange2 = new StringBuilder();
|
||||||
highlightedChange2.append(CURLY_LEFT);
|
highlightedChange2.append(CURLY_LEFT);
|
||||||
highlightedChange2.append(COLOR_HIGHLIGHT);
|
highlightedChange2.append(COLOR_HIGHLIGHT);
|
||||||
highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex());
|
highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex());
|
||||||
highlightedChange2.append(CURLY_RIGHT);
|
highlightedChange2.append(CURLY_RIGHT);
|
||||||
latex.append(original.replace(new LatexCreatorType(s.getVariable()).getLatex(),
|
latex.append(original.replace(originalType, highlightedChange2.toString()));
|
||||||
highlightedChange2.toString()));
|
} else {
|
||||||
|
latex.append(sb.toString());
|
||||||
|
}
|
||||||
} else {
|
} else {
|
||||||
latex.append(sb.toString());
|
latex.append(sb.toString());
|
||||||
}
|
}
|
||||||
|
@ -20,7 +20,7 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
|
|||||||
* clipboard. Each InferenceRuleField is displayed in drawer area of the web page.
|
* clipboard. Each InferenceRuleField is displayed in drawer area of the web page.
|
||||||
*/
|
*/
|
||||||
@CssImport("./styles/view/main/inference-rule-field.css")
|
@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 {
|
public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver {
|
||||||
|
|
||||||
private static final long serialVersionUID = -8551851183297707985L;
|
private static final long serialVersionUID = -8551851183297707985L;
|
||||||
|
@ -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.
|
* Contains components which allow the user to enter a lambda term and start the type inference algorithm.
|
||||||
*/
|
*/
|
||||||
@CssImport("./styles/view/main/input-bar.css")
|
@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 {
|
public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||||
private static final long serialVersionUID = -6099700300418752958L;
|
private static final long serialVersionUID = -6099700300418752958L;
|
||||||
|
|
||||||
@ -66,17 +66,9 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
inputField.setMaxLength(MAX_INPUT_LENGTH);
|
inputField.setMaxLength(MAX_INPUT_LENGTH);
|
||||||
|
|
||||||
// attach a listener that replaces \ with λ
|
// attach a listener that replaces \ with λ
|
||||||
// JavaScript is used because Vaadin does not have APIs for selectionStart/selectionEnd
|
// JavaScript is used because this is a latency-sensitive operation
|
||||||
UI.getCurrent().getPage().executeJs(
|
// (and Vaadin does not have APIs for selectionStart/selectionEnd)
|
||||||
"document.getElementById('" + INPUT_FIELD_ID + "').addEventListener('keyup', e => {"
|
UI.getCurrent().getPage().executeJs("window.backslashListener($0);", INPUT_FIELD_ID);
|
||||||
+ "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;"
|
|
||||||
+ "}});");
|
|
||||||
Button lambdaButton = new Button(getTranslation("root.lambda"));
|
Button lambdaButton = new Button(getTranslation("root.lambda"));
|
||||||
lambdaButton.setId(LAMBDA_BUTTON_ID);
|
lambdaButton.setId(LAMBDA_BUTTON_ID);
|
||||||
UI.getCurrent().getPage().executeJs("window.lambdaButtonListener($0, $1);", LAMBDA_BUTTON_ID, INPUT_FIELD_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() {
|
private void onTypeInferButtonClick() {
|
||||||
UI.getCurrent().getPage()
|
|
||||||
.executeJs("return document.getElementById($0).shadowRoot.querySelector('input').value", INPUT_FIELD_ID)
|
|
||||||
.then(String.class, value -> {
|
|
||||||
inputField.blur();
|
inputField.blur();
|
||||||
callback.accept(Pair.of(value, typeAssumptionsArea.getTypeAssumptions()));
|
callback.accept(Pair.of(inputField.getValue(), typeAssumptionsArea.getTypeAssumptions()));
|
||||||
});
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private void onTypeAssumptionsButton() {
|
private void onTypeAssumptionsButton() {
|
||||||
|
@ -22,7 +22,7 @@ import java.util.function.Consumer;
|
|||||||
* Represents a single type assumption input component.
|
* Represents a single type assumption input component.
|
||||||
* Each TypeAssumptionField is displayed in the TypeAssumptionsArea.
|
* 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("./styles/view/main/type-assumption-field.css")
|
||||||
@CssImport(value = "./styles/view/main/type-assumption-input-field.css", themeFor = "vaadin-text-field")
|
@CssImport(value = "./styles/view/main/type-assumption-input-field.css", themeFor = "vaadin-text-field")
|
||||||
public class TypeAssumptionField extends HorizontalLayout implements LocaleChangeObserver {
|
public class TypeAssumptionField extends HorizontalLayout implements LocaleChangeObserver {
|
||||||
|
@ -10,7 +10,6 @@
|
|||||||
"noImplicitReturns": true,
|
"noImplicitReturns": true,
|
||||||
"noImplicitAny": true,
|
"noImplicitAny": true,
|
||||||
"noImplicitThis": true,
|
"noImplicitThis": true,
|
||||||
"noUnusedLocals": true,
|
|
||||||
"noUnusedParameters": true,
|
"noUnusedParameters": true,
|
||||||
"experimentalDecorators": true
|
"experimentalDecorators": true
|
||||||
},
|
},
|
||||||
|
Loading…
Reference in New Issue
Block a user