arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-09-16 16:55:08 +00:00
Code Issues Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Moritz Dieing 2021-09-29 17:11:53 +02:00
commit 1def7789d6
12 changed files with 57 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
frontend/src/copy-to-clipboard.ts
View File

@ -1,3 +1,4 @@
// utility function to copy e.g. the LaTeX code into the user's clipboard
// @ts-ignore
window.copyToClipboard = (text: string) => {
const textarea = document.createElement("textarea");

5
frontend/src/input-bar-enhancements.ts
View File

@ -1,5 +1,5 @@
function changeEvent(element: HTMLElement, inputID: string) {
// notify Vaadin
// notify Vaadin about the text value change
// @ts-ignore
document.getElementById(inputID)!.__dataValue.value = element.value;
const evt = new Event("change", { bubbles: true });
@ -8,6 +8,8 @@ function changeEvent(element: HTMLElement, inputID: string) {
// @ts-ignore
window.buttonListener = (buttonID: string, inputID: string) => {
// this function is called when the lambda button or the ∀ button is pressed
// the requested character is inserted at the cursor position
let replacement = (buttonID === "lambda-button") ? 'λ' : '∀';
const button = document.getElementById(buttonID)!;
const input = document.getElementById(inputID)!;
@ -24,6 +26,7 @@ window.buttonListener = (buttonID: string, inputID: string) => {
// @ts-ignore
window.characterListener = (inputID: string) => {
// called when the user types in one of the input fields (see InputBar.java)
let toReplace = (inputID === "term-input-field") ? '\\' : '!';
let replacement = (inputID === "term-input-field") ? 'λ' : '∀';
document.getElementById(inputID)!.addEventListener('keyup', e => {

4
frontend/src/key-shortcuts.ts
View File

@ -1,10 +1,12 @@
// register a global listener for key events
document.onkeydown = handleKey;
function handleKey(e: KeyboardEvent) {
if ((e.target! as HTMLElement).tagName.toLowerCase() === "vaadin-text-field") {
return;
return; // don't process text input
}
let element = null;
// these shortcuts are documented in the help dialog
if (e.code === "ArrowLeft") {
// left arrow
if (!e.ctrlKey) {

2
frontend/src/mathjax-adapter.ts
View File

@ -1,6 +1,7 @@
import {LitElement, html} from 'lit-element';
import {TemplateResult} from "lit-html";
// TypeScript declarations, only used to typecheck the code
declare let window: {
MathJax: {
typesetShadow: (shadowRoot: ShadowRoot, callback: () => void) => void,
@ -9,6 +10,7 @@ declare let window: {
addEventListener: (event: string, listener: () => void) => void;
};
// base class that can typeset content added to it
export abstract class MathjaxAdapter extends LitElement {
private execTypeset(shadowRoot: ShadowRoot, extraData: any) {
if (window.MathJax) {

1
frontend/src/mathjax-display.ts
View File

@ -1,5 +1,6 @@
import {MathjaxAdapter} from "./mathjax-adapter";
// really basic class that only displays some static LaTeX code
class MathjaxDisplay extends MathjaxAdapter {
connectedCallback() {
super.connectedCallback();

10
frontend/src/mathjax-explanation.ts
View File

@ -2,6 +2,8 @@ import {MathjaxAdapter} from "./mathjax-adapter";
class MathjaxExplanation extends MathjaxAdapter {
private lastStepShown: number = 0
static readonly opacityInactive: string = "0.5"
static readonly opacityActive: string = "1.0"
connectedCallback() {
super.connectedCallback();
@ -16,6 +18,7 @@ class MathjaxExplanation extends MathjaxAdapter {
protected calculateSteps(_extraData: any) {
let stepIdx = 0;
// find all of the rendered steps and register click listeners
for (let text of this.shadowRoot!.querySelectorAll<HTMLElement>(".tc-text")) {
let thisStepIdx = stepIdx;
stepIdx++;
@ -28,20 +31,21 @@ class MathjaxExplanation extends MathjaxAdapter {
this.scrollToElementIfNeeded(text);
continue;
}
text.style.opacity = "0.5";
text.style.opacity = MathjaxExplanation.opacityInactive;
}
}
protected showStep(n: number): void {
// lower the opacity of the previously active step and show the next one
let lastEl = this.getElementForStep(this.lastStepShown);
if (lastEl) {
lastEl.style.opacity = "0.5";
lastEl.style.opacity = MathjaxExplanation.opacityInactive;
}
let el = this.getElementForStep(n);
this.lastStepShown = n;
if (el) {
this.scrollToElementIfNeeded(el);
el.style.opacity = "1.0";
el.style.opacity = MathjaxExplanation.opacityActive;
}
}

42
frontend/src/mathjax-proof-tree.ts
View File

@ -1,6 +1,7 @@
import {MathjaxAdapter} from "./mathjax-adapter";
import {hoverAreaAroundElements} from "./mathjax-style-hacks";
// Typescript declaration of the svg-pan-zoom library used
declare let window: {
svgPanZoomFun: (svg: SVGElement, options: {
fit: boolean;
@ -28,11 +29,13 @@ declare global {
}
}
// methods declared in the Java class
interface ProofTreeServer {
setStepCount: (count: number) => void;
}
class MathjaxProofTree extends MathjaxAdapter {
// list of the SVG elements that make up each step in the proof tree
private steps: [SVGElement, SVGElement[]][] = [];
private $server: ProofTreeServer | undefined;
// the element used as tooltip background
@ -43,7 +46,9 @@ class MathjaxProofTree extends MathjaxAdapter {
// true if the user is currently moving the proof tree around
private panningSvg: boolean = false;
private hoveringOnElement: SVGGraphicsElement | null = null;
// CSS elements used to highlight types etc.
private hoverStyles: HTMLElement | null = null;
// (in the unification element too)
private hoverStylesUnification: HTMLElement | null = null;
protected showStep(n: number): void {
@ -62,6 +67,8 @@ class MathjaxProofTree extends MathjaxAdapter {
}
private analyzeSvgStructure() {
// this function process the MathJax output, performs some display corrections and finally determines which
// SVG elements belong to which step
const semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
const inferenceRuleSelector = 'g[semantics="bspr_inferenceRule:down"]';
const labelSelector = 'g[semantics="bspr_prooflabel:left"]';
@ -77,6 +84,7 @@ class MathjaxProofTree extends MathjaxAdapter {
root = root.parentNode! as SVGElement;
}
// first, enumerate all of the steps
// and assign IDs
let stepIdx = 0;
for (const a of [root, ...root.querySelectorAll<SVGElement>("g[semantics]")]) {
let semantics = a.getAttribute("semantics")!;
@ -86,7 +94,7 @@ class MathjaxProofTree extends MathjaxAdapter {
stepIdx++;
}
}
// then create the steps
// then create the steps list
let steps: [SVGElement, SVGElement[]][] = [];
stepIdx = 0;
for (const a of [root, ...root.querySelectorAll<SVGElement>("g[semantics]")]) {
@ -150,7 +158,6 @@ class MathjaxProofTree extends MathjaxAdapter {
// in each row, the elements are arranged to not overlap
// 2. place inference conclusions under the center of their line
const nodeIterator = [...root.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']," + inferenceRuleSelector)];
console.log(`working with ${nodeIterator.length} nodes`);
// start layout fixes in the innermost part of the SVG
nodeIterator.reverse();
for (const row of nodeIterator) {
@ -250,7 +257,7 @@ class MathjaxProofTree extends MathjaxAdapter {
// svg-pan-zoom should not be used on empty SVGs
if (nodeIterator.length >= 3) {
// a timeout is required, otherwise the proof tree is moved around
// a timeout is required, otherwise the proof tree is moved around..
setTimeout(() => {
this.setupPanZoom(this.shadowRoot!, svg);
}, 100);
@ -280,7 +287,7 @@ class MathjaxProofTree extends MathjaxAdapter {
// Handle double tap
// @ts-ignore
this.hammer.on('doubletap', () => {
options.instance.zoomIn()
options.instance.zoomIn();
});
let pannedX = 0;
@ -304,14 +311,9 @@ class MathjaxProofTree extends MathjaxAdapter {
if (explainer) {
const ctm1 = svg.getBoundingClientRect();
const ctm2 = this.defElBackground!.getBoundingClientRect();
explainer.style.left = (ctm2.left - ctm1.left) + "px";
explainer.style.top = (ctm2.bottom - ctm1.top) + "px";
// TODO(performance): this should be more efficient, but somehow flickers
/*
const dx = (ctm2.left - ctm1.left) - explainer.offsetLeft;
const dy = (ctm2.bottom - ctm1.top) - explainer.offsetTop;
explainer.style.transform = "translate(" + dx + "px," + dy + "px)";
*/
const dx = (ctm2.left - ctm1.left) - explainer.offsetLeft;
const dy = (ctm2.bottom - ctm1.top) - explainer.offsetTop;
explainer.style.transform = "translate(" + dx + "px," + dy + "px)";
}
});
// @ts-ignore
@ -423,6 +425,7 @@ class MathjaxProofTree extends MathjaxAdapter {
}
let typeTarget = e.target! as SVGGraphicsElement;
let counter = 0;
// try to find a relevant element in the tree
while (typeTarget.classList
&& !typeTarget.classList.contains("typicalc-type")
&& !typeTarget.classList.contains("typicalc-label")) {
@ -435,6 +438,8 @@ class MathjaxProofTree extends MathjaxAdapter {
if (!typeTarget.classList) {
return;
}
// hover over step label => show tooltip of definition, highlight constraints added
// hover over type => highlight it everywhere
let isType = typeTarget.classList.contains("typicalc-type");
let isLabel = typeTarget.classList.contains("typicalc-label");
if (mouseIn) {
@ -453,6 +458,7 @@ class MathjaxProofTree extends MathjaxAdapter {
}
let stepIndex = stepTarget.getAttribute("typicalc") === "step" ? Number(stepTarget.id.substring(4)) : -1;
// un-hide the definition text
const defId = typeTarget.classList[1].replace("-label-", "-definition-");
const defEl = this.shadowRoot!.getElementById(defId)! as unknown as SVGGraphicsElement;
const transform = viewport.getTransformToElement(typeTarget);
@ -462,6 +468,7 @@ class MathjaxProofTree extends MathjaxAdapter {
const svgRect = defEl.getBBox();
defEl.transform.baseVal[0].matrix.e = -transform.e - svgRect.width + offsetX + 1000;
defEl.transform.baseVal[0].matrix.f = -transform.f - 5500 + offsetY;
// create the yellow tooltip background
this.defElBackground = root.getElementById(this.hoverTextBackgroundElID) as SVGRectElement | null;
if (!this.defElBackground) {
this.defElBackground = document.createElementNS("http://www.w3.org/2000/svg", "rect");
@ -488,10 +495,11 @@ class MathjaxProofTree extends MathjaxAdapter {
p.style.top = (ctm2.bottom - ctm1.top) + "px";
p.style.backgroundColor = "white";
p.style.padding = "5px";
p.innerText = data[stepIndex];
p.innerText = data[stepIndex]; // add custom data to tooltip
// @ts-ignore
window.MathJax.typesetPromise([p])
.then(() => {
// add rendered custom text to the main tooltip
const svgRect2 = this.defElBackground!.getBBox();
const svgP = p.getElementsByTagName("svg")[0];
@ -567,9 +575,15 @@ class MathjaxProofTree extends MathjaxAdapter {
const exp = explainers[explainers.length - 1];
exp.parentNode!.removeChild(exp);
}
// hide definition texts
this.shadowRoot!
.querySelectorAll<SVGGraphicsElement>(".typicalc-definition")!
.forEach((it) => it.style.display = "none");
.forEach((it) => {
if (it.style) {
it.style.display = "none"
}
});
// remove the tooltip background
let defElBackground = this.shadowRoot!.getElementById(this.hoverTextBackgroundElID);
if (defElBackground) {
defElBackground.parentElement!.removeChild(defElBackground);

5
frontend/src/mathjax-setup.js
View File

@ -3,6 +3,7 @@
SVGElement.prototype.getTransformToElement = SVGElement.prototype.getTransformToElement || function(elem) {
return elem.getScreenCTM().inverse().multiply(this.getScreenCTM());
};
// MathJax configuration boilerplate and ShadowDOM adapter
window.MathJax = {
loader: {
load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/color', '[tex]/html', '[tex]/textmacros', '[tex]/unicode']
@ -112,13 +113,13 @@ window.MathJax = {
bubbles: true,
composed: true,
detail: "composed"
})
});
MathJax.startup.defaultReady();
MathJax.startup.promise.then(() => {
console.log("MathJax initialized");
MathJax.isInitialized = true;
document.dispatchEvent(event);
})
});
}
}
};

3
frontend/src/mathjax-style-hacks.ts
View File

@ -1,3 +1,6 @@
// to ease hovering above step labels and types, we increase the usable target area
// in the case of Firefox, we add an invisible stroke to the SVG element
// in the case of Chrome, we set the pointer-events area to the rectangular bounding box of the element
export const hoverAreaAroundElements: string = `
.typicalc-type, g[semantics='bspr_prooflabel:left'] {
/* cross-browser-compatibility: Chrome does not support the stroke trick, but instead bounding-box (which is not supported by Firefox..) */

1
frontend/src/share-dialog-autoselect.ts
View File

@ -1,5 +1,6 @@
// @ts-ignore
window.autoSelect = (className: string) => {
// select entire text when the field is focused
let el = document.getElementsByClassName(className);
Array.from(el).forEach(field => {
field.addEventListener('focus', event => {

2
frontend/src/type-input-listener.ts
View File

@ -1,3 +1,5 @@
// this listener is used in the type assumptions input field to subscript type indices etc.
const subscripted = [...'\u2080\u2081\u2082\u2083\u2084\u2085\u2086\u2087\u2088\u2089'];
// @ts-ignore

2
frontend/styles/view/main/upper-bar.css
View File

@ -20,6 +20,8 @@
#input-bar {
width: 75%;
/* require a larger width on small screens! */
min-width: min(100%, 1100px);
flex-grow: 1;
align-items: flex-end;
padding: 0 1em;