From c7bb826b73bc5da60555c7aedc77e321c07a2727 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 31 Aug 2021 11:33:47 +0200 Subject: [PATCH] Improve performance of proof tree panning --- frontend/src/mathjax-proof-tree.ts | 117 ++++++++++++------ .../MathjaxProofTree.java | 15 +++ 2 files changed, 92 insertions(+), 40 deletions(-) diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index 031c6ed..bab4dd1 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/frontend/src/mathjax-proof-tree.ts @@ -39,6 +39,12 @@ class MathjaxProofTree extends MathjaxAdapter { private defElBackground: SVGRectElement | null = null; // CSS class used for the tooltip element private hoverTextElID: string = "typicalc-hover-explainer"; + private hoverTextBackgroundElID: string = "typicalc-tooltip-background"; + // true if the user is currently moving the proof tree around + private panningSvg: boolean = false; + private hoveringOnElement: SVGGraphicsElement | null = null; + private hoverStyles: HTMLElement | null = null; + private hoverStylesUnification: HTMLElement | null = null; protected showStep(n: number): void { for (let current = 0; current < this.steps.length; current++) { @@ -266,8 +272,9 @@ class MathjaxProofTree extends MathjaxAdapter { this.hammer.on('panstart panmove', ev => { // On pan start reset panned variables if (ev.type === 'panstart') { - pannedX = 0 - pannedY = 0 + pannedX = 0; + pannedY = 0; + this.panningSvg = true; } // Pan only the difference @@ -289,6 +296,10 @@ class MathjaxProofTree extends MathjaxAdapter { */ } }); + // @ts-ignore + this.hammer.on("panend", (e) => { + this.panningSvg = false; + }); let initialScale = 1; // Handle pinch @@ -328,6 +339,20 @@ class MathjaxProofTree extends MathjaxAdapter { let matrix = svg.getElementById("svg-pan-zoom-controls")!.transform.baseVal[0].matrix; matrix.e = 0; matrix.f = 0; + + svg.addEventListener("mousemove", (e) => { + if (!this.hoveringOnElement || this.panningSvg) { + return; + } + const x1 = e.clientX; + const y1 = e.clientY; + const rect = this.hoveringOnElement.getBoundingClientRect(); + const x2 = (rect.left + rect.right) / 2; + const y2 = (rect.top + rect.bottom) / 2; + if ((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > (rect.width*rect.width)) { // use relative distance + this.destroyTooltip(); + } + }); } this.steps = steps; this.showStep(0); @@ -343,18 +368,18 @@ class MathjaxProofTree extends MathjaxAdapter { const svg = root.querySelector("svg")!; // setup style container for styles applied on hover - let hoverStyles = root.querySelector("#typicalc-hover-styles"); - if (!hoverStyles) { - hoverStyles = document.createElement('style'); - hoverStyles.id = "typicalc-hover-styles"; - root.querySelector("mjx-head")!.appendChild(hoverStyles); + this.hoverStyles = root.querySelector("#typicalc-hover-styles"); + if (!this.hoverStyles) { + this.hoverStyles = document.createElement('style'); + this.hoverStyles.id = "typicalc-hover-styles"; + root.querySelector("mjx-head")!.appendChild(this.hoverStyles); } const unificationEl = root.host.parentElement!.parentElement!.querySelector("tc-unification")!; - let hoverStylesUnification = unificationEl.shadowRoot!.querySelector("#typicalc-hover-styles"); - if (!hoverStylesUnification) { - hoverStylesUnification = document.createElement('style'); - hoverStylesUnification.id = "typicalc-hover-styles"; - unificationEl.shadowRoot!.querySelector("mjx-head")!.appendChild(hoverStylesUnification); + this.hoverStylesUnification = unificationEl.shadowRoot!.querySelector("#typicalc-hover-styles"); + if (!this.hoverStylesUnification) { + this.hoverStylesUnification = document.createElement('style'); + this.hoverStylesUnification.id = "typicalc-hover-styles"; + unificationEl.shadowRoot!.querySelector("mjx-head")!.appendChild(this.hoverStylesUnification); } // set the size of the rendered SVG to the size of the container element if (!root.querySelector("#style-fixes")) { @@ -366,8 +391,7 @@ class MathjaxProofTree extends MathjaxAdapter { mjx-container {\ margin: 0 !important;\ }\ - #typicalc-definition-abs, #typicalc-definition-abs-let, #typicalc-definition-app,\ - #typicalc-definition-const, #typicalc-definition-var, #typicalc-definition-var-let, #typicalc-definition-let {\ + .typicalc-definition {\ display: none;\ border: 2px solid red;\ }" + hoverAreaAroundElements; @@ -378,6 +402,9 @@ class MathjaxProofTree extends MathjaxAdapter { const viewport = svg.querySelector("#step0")!.parentNode as SVGGraphicsElement; const handleMouseEvent = (e: MouseEvent, mouseIn: boolean) => { + if (this.panningSvg) { + return; // do not add/remove the tooltip if the user is moving the proof tree around + } let typeTarget = e.target! as SVGGraphicsElement; let counter = 0; while (typeTarget.classList @@ -395,11 +422,13 @@ class MathjaxProofTree extends MathjaxAdapter { let isType = typeTarget.classList.contains("typicalc-type"); let isLabel = typeTarget.classList.contains("typicalc-label"); if (mouseIn) { + this.destroyTooltip(); + this.hoveringOnElement = typeTarget; if (isType) { const typeClass = typeTarget.classList[1]; const css = "." + typeClass + " { color: red; }"; - hoverStyles!.innerHTML = css; - hoverStylesUnification!.innerHTML = css; + this.hoverStyles!.innerHTML = css; + this.hoverStylesUnification!.innerHTML = css; } else if (isLabel) { let stepTarget = typeTarget; while (stepTarget.getAttribute("typicalc") !== "step" && counter < 15) { @@ -417,19 +446,19 @@ 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; - this.defElBackground = root.getElementById(defId + "-background") as SVGRectElement | null; + this.defElBackground = root.getElementById(this.hoverTextBackgroundElID) as SVGRectElement | null; if (!this.defElBackground) { this.defElBackground = document.createElementNS("http://www.w3.org/2000/svg", "rect"); - this.defElBackground.id = defId + "-background"; + this.defElBackground.id = this.hoverTextBackgroundElID; this.defElBackground.setAttribute("x", "0"); this.defElBackground.setAttribute("y", "0"); - this.defElBackground.setAttribute("width", String(svgRect.width + 2000)); defEl.parentElement!.insertBefore(this.defElBackground, defEl); } this.defElBackground.setAttribute("x", String(-transform.e - svgRect.width + offsetX)); const defElBackgroundY = -transform.f - 7000 + offsetY; this.defElBackground.setAttribute("y", String(defElBackgroundY)); const defElBackgroundHeight = svgRect.height + 1000; + this.defElBackground.setAttribute("width", String(svgRect.width + 2000)); this.defElBackground.setAttribute("height", String(defElBackgroundHeight)); this.defElBackground.setAttribute("fill", "yellow"); // calculate screen coordinates @@ -480,30 +509,12 @@ class MathjaxProofTree extends MathjaxAdapter { if (typeTarget.classList.length >= 3) { const stepId = typeTarget.classList[2]; - hoverStylesUnification!.innerHTML = "." + stepId + " { color: red; }"; + this.hoverStylesUnification!.innerHTML = "." + stepId + " { color: red; }"; } } } else { - if (isType) { - hoverStyles!.innerHTML = ""; - hoverStylesUnification!.innerHTML = ""; - } else if (isLabel) { - // remove previous tooltip, if possible - let explainers = svg.getElementsByClassName(this.hoverTextElID); - // do not use a for..of loop, it won't work - while (explainers.length > 0) { - const exp = explainers[0]; - exp.parentNode!.removeChild(exp); - } - const defId = typeTarget.classList[1].replace("-label-", "-definition-"); - this.shadowRoot!.getElementById(defId)!.style.display = "none"; - let defElBackground = this.shadowRoot!.getElementById(defId + "-background"); - defElBackground!.setAttribute("y", String(-10000)); - defElBackground!.setAttribute("fill", "transparent"); - if (typeTarget.classList.length >= 3) { - hoverStylesUnification!.innerHTML = ""; - } - } + this.hoveringOnElement = null; + this.destroyTooltip(); } }; // listen for hover events on types @@ -522,6 +533,32 @@ class MathjaxProofTree extends MathjaxAdapter { this.$server!.setStepCount(this.steps.length); } + + private destroyTooltip() { + const svg = this.shadowRoot!.querySelector("svg"); + if (!svg) { + return; + } + + // remove type highlighting + this.hoverStyles!.innerHTML = ""; + this.hoverStylesUnification!.innerHTML = ""; + + // remove previous tooltip, if possible + let explainers = svg.getElementsByClassName(this.hoverTextElID); + // do not use a for..of loop, it won't work + while (explainers.length > 0) { + const exp = explainers[explainers.length - 1]; + exp.parentNode!.removeChild(exp); + } + this.shadowRoot! + .querySelectorAll(".typicalc-definition")! + .forEach((it) => it.style.display = "none"); + let defElBackground = this.shadowRoot!.getElementById(this.hoverTextBackgroundElID); + if (defElBackground) { + defElBackground.parentElement!.removeChild(defElBackground); + } + } } customElements.define('tc-proof-tree', MathjaxProofTree); diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java index d459732..2d3c40e 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java @@ -36,28 +36,43 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter { * @param extraData extra data to pass to the frontend script */ public MathjaxProofTree(String latex, List extraData) { + // step definitions used for tooltips content.add("\\[\\cssId{typicalc-prooftree}{" + latex + "}" + + "\\class{typicalc-definition}{" + "\\cssId{typicalc-definition-abs}{" + getTranslation("root.absLatex") + "}" + + "}" + + "\\class{typicalc-definition}{" + "\\cssId{typicalc-definition-abs-let}{" + getTranslation("root.absLetLatex") + "}" + + "}" + + "\\class{typicalc-definition}{" + "\\cssId{typicalc-definition-app}{" + getTranslation("root.appLatex") + "}" + + "}" + + "\\class{typicalc-definition}{" + "\\cssId{typicalc-definition-const}{" + getTranslation("root.constLatex") + "}" + + "}" + + "\\class{typicalc-definition}{" + "\\cssId{typicalc-definition-var}{" + getTranslation("root.varLatex") + "}" + + "}" + + "\\class{typicalc-definition}{" + "\\cssId{typicalc-definition-var-let}{" + getTranslation("root.varLetLatex") + "}" + + "}" + + "\\class{typicalc-definition}{" + "\\cssId{typicalc-definition-let}{" + getTranslation("root.letLatex") + "}" + + "}" + "\\]"); getElement().callJsFunction("requestTypeset", new Gson().toJson(extraData)); }