From 91daed42c4602371ecc8560df8646de49acaaa52 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 29 Sep 2021 10:15:51 +0200 Subject: [PATCH 1/2] Optimize frontend script and style --- frontend/src/mathjax-proof-tree.ts | 17 ++++++++--------- frontend/styles/view/main/upper-bar.css | 2 ++ 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index 2b536b5..431d2cd 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/frontend/src/mathjax-proof-tree.ts @@ -304,14 +304,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 @@ -569,7 +564,11 @@ class MathjaxProofTree extends MathjaxAdapter { } this.shadowRoot! .querySelectorAll(".typicalc-definition")! - .forEach((it) => it.style.display = "none"); + .forEach((it) => { + if (it.style) { + it.style.display = "none" + } + }); let defElBackground = this.shadowRoot!.getElementById(this.hoverTextBackgroundElID); if (defElBackground) { defElBackground.parentElement!.removeChild(defElBackground); diff --git a/frontend/styles/view/main/upper-bar.css b/frontend/styles/view/main/upper-bar.css index 8898f3a..3a98600 100644 --- a/frontend/styles/view/main/upper-bar.css +++ b/frontend/styles/view/main/upper-bar.css @@ -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; From edafdf0ff4c37de109a59163b65e938eef19af80 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 29 Sep 2021 10:57:00 +0200 Subject: [PATCH 2/2] Document frontend scripts --- frontend/src/copy-to-clipboard.ts | 1 + frontend/src/input-bar-enhancements.ts | 5 ++++- frontend/src/key-shortcuts.ts | 4 +++- frontend/src/mathjax-adapter.ts | 2 ++ frontend/src/mathjax-display.ts | 1 + frontend/src/mathjax-explanation.ts | 10 +++++++--- frontend/src/mathjax-proof-tree.ts | 25 ++++++++++++++++++++----- frontend/src/mathjax-setup.js | 5 +++-- frontend/src/mathjax-style-hacks.ts | 3 +++ frontend/src/share-dialog-autoselect.ts | 1 + frontend/src/type-input-listener.ts | 2 ++ 11 files changed, 47 insertions(+), 12 deletions(-) diff --git a/frontend/src/copy-to-clipboard.ts b/frontend/src/copy-to-clipboard.ts index 726fd03..bafb4e5 100644 --- a/frontend/src/copy-to-clipboard.ts +++ b/frontend/src/copy-to-clipboard.ts @@ -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"); diff --git a/frontend/src/input-bar-enhancements.ts b/frontend/src/input-bar-enhancements.ts index a9dc2c1..6ba8bc0 100644 --- a/frontend/src/input-bar-enhancements.ts +++ b/frontend/src/input-bar-enhancements.ts @@ -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 => { diff --git a/frontend/src/key-shortcuts.ts b/frontend/src/key-shortcuts.ts index 433c75c..39822ad 100644 --- a/frontend/src/key-shortcuts.ts +++ b/frontend/src/key-shortcuts.ts @@ -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) { diff --git a/frontend/src/mathjax-adapter.ts b/frontend/src/mathjax-adapter.ts index 82c87d8..a4daead 100644 --- a/frontend/src/mathjax-adapter.ts +++ b/frontend/src/mathjax-adapter.ts @@ -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) { diff --git a/frontend/src/mathjax-display.ts b/frontend/src/mathjax-display.ts index 958ddf5..7e2f873 100644 --- a/frontend/src/mathjax-display.ts +++ b/frontend/src/mathjax-display.ts @@ -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(); diff --git a/frontend/src/mathjax-explanation.ts b/frontend/src/mathjax-explanation.ts index 99aeed8..0400cda 100644 --- a/frontend/src/mathjax-explanation.ts +++ b/frontend/src/mathjax-explanation.ts @@ -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(".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; } } diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index 431d2cd..0ce2457 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/frontend/src/mathjax-proof-tree.ts @@ -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("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("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("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; @@ -418,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")) { @@ -430,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) { @@ -448,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); @@ -457,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"); @@ -483,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]; @@ -562,6 +575,7 @@ class MathjaxProofTree extends MathjaxAdapter { const exp = explainers[explainers.length - 1]; exp.parentNode!.removeChild(exp); } + // hide definition texts this.shadowRoot! .querySelectorAll(".typicalc-definition")! .forEach((it) => { @@ -569,6 +583,7 @@ class MathjaxProofTree extends MathjaxAdapter { it.style.display = "none" } }); + // remove the tooltip background let defElBackground = this.shadowRoot!.getElementById(this.hoverTextBackgroundElID); if (defElBackground) { defElBackground.parentElement!.removeChild(defElBackground); diff --git a/frontend/src/mathjax-setup.js b/frontend/src/mathjax-setup.js index 1c51320..d140dcf 100644 --- a/frontend/src/mathjax-setup.js +++ b/frontend/src/mathjax-setup.js @@ -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); - }) + }); } } }; diff --git a/frontend/src/mathjax-style-hacks.ts b/frontend/src/mathjax-style-hacks.ts index e446f47..9fc83cc 100644 --- a/frontend/src/mathjax-style-hacks.ts +++ b/frontend/src/mathjax-style-hacks.ts @@ -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..) */ diff --git a/frontend/src/share-dialog-autoselect.ts b/frontend/src/share-dialog-autoselect.ts index 36bc849..67031eb 100644 --- a/frontend/src/share-dialog-autoselect.ts +++ b/frontend/src/share-dialog-autoselect.ts @@ -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 => { diff --git a/frontend/src/type-input-listener.ts b/frontend/src/type-input-listener.ts index b83b083..e59a7f6 100644 --- a/frontend/src/type-input-listener.ts +++ b/frontend/src/type-input-listener.ts @@ -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