import {MathjaxAdapter} from "./mathjax-adapter"; declare let window: { svgPanZoomFun: (svg: SVGElement, options: { fit: boolean; controlIconsEnabled: boolean; customEventsHandler: { init: (options: any) => void; haltEventListeners: string[]; destroy: () => void }; }) => void; } // these attributes and functions are supported by major browsers, but TS does not know about them declare global { interface SVGElement { getElementById: (id: string) => SVGGraphicsElement | null; viewBox: SVGAnimatedRect; } interface SVGGraphicsElement { getTransformToElement: (other: SVGGraphicsElement) => SVGMatrix; } interface SVGTransformList { [index: number]: SVGTransform; } } interface ProofTreeServer { setStepCount: (count: number) => void; } class MathjaxProofTree extends MathjaxAdapter { private steps: [SVGElement, SVGElement[]][] = []; private $server: ProofTreeServer | undefined; protected showStep(n: number): void { for (let current = 0; current < this.steps.length; current++) { this.steps[current][0].style.display = "none"; for (const node of this.steps[current][1]) { node.style.display = "none"; } } for (let current = 0; current < this.steps.length && current <= n; current++) { this.steps[current][0].style.display = ""; for (const node of this.steps[current][1]) { node.style.display = ""; } } } protected calculateSteps(): void { const semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0; const inferenceRuleSelector = 'g[semantics="bspr_inferenceRule:down"]'; const labelSelector = 'g[semantics="bspr_prooflabel:left"]'; const stepSelector = 'g[typicalc="step"]'; // space between inference premises const padding = 300; console.log("calculating steps.."); if (this.shadowRoot !== null) { console.time('stepCalculation'); const root = this.shadowRoot; // first, enumerate all of the steps let stepIdx = 0; for (const a of root.querySelectorAll("g[semantics]")) { let semantics = a.getAttribute("semantics")!; if (semanticsMatch(semantics)) { a.setAttribute("typicalc", "step"); a.setAttribute("id", "step" + stepIdx); stepIdx++; } } // then create the steps let steps: [SVGElement, SVGElement[]][] = []; stepIdx = 0; for (const a of root.querySelectorAll("g[semantics]")) { let semantics = a.getAttribute("semantics")!; if (semanticsMatch(semantics)) { const id = "step" + stepIdx; const idSelector = `#${id} `; stepIdx++; // find the next one/two steps above this one const aboveStep1 = a.querySelector(idSelector + stepSelector); let above = []; if (aboveStep1 != null) { const parent = aboveStep1.parentElement!.parentElement!; parent.setAttribute("id", "typicalc-selector"); for (const node of parent.querySelectorAll('#typicalc-selector > g > ' + stepSelector)) { above.push(node); } parent.removeAttribute("id"); } const rule = a.querySelector(idSelector + inferenceRuleSelector); if (rule !== null) { let i = 0; for (const node of rule.children) { if (i !== 1) { above.push(node as SVGElement); } i += 1; } } const label = a.querySelector(idSelector + labelSelector); if (label) { above.push(label); } if (stepIdx === 1) { // initial step should not show premises steps.push([a, []]); } steps.push([a, above]); } } const svg = root.querySelector("svg")!; // limit start zoom svg.viewBox.baseVal.width = Math.min(100000, svg.viewBox.baseVal.width); svg.viewBox.baseVal.width = Math.max(20000, svg.viewBox.baseVal.width); // MathJax layout of bussproofs is sometimes wrong: // https://github.com/mathjax/MathJax/issues/2270 // https://github.com/mathjax/MathJax/issues/2626 // we fix it in two phases (executed at the same time): // 1. fix overlapping by iterating over "rows" in the SVG created by MathJax // in each row, the elements are arranged to not overlap // 2. place inference conclusions under the center of their line const nodeIterator = [...svg.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) { const semantics = row.getAttribute("semantics"); if (semantics === "bspr_inferenceRule:down") { const conclusion = row.children[1].querySelector('g[data-mml-node="mstyle"]')!; const conclusionBox = conclusion.getBBox(); const line = row.children[2] as SVGGraphicsElement; const bbox = line.getBBox(); const offset2 = line.getTransformToElement(conclusion); let dx = bbox.width / 2 + offset2.e - conclusionBox.width / 2; dx += Number(line.getAttribute("x1")); let table = row.parentNode as SVGGraphicsElement; let prevNode; let magicNumber = 0; while (table.getAttribute("semantics") !== "bspr_inferenceRule:down") { prevNode = table; table = table.parentNode as SVGGraphicsElement; if (table.getAttribute("data-mml-node") === "mtr" && table.childNodes.length === 3) { for (let i = 0; i < table.childNodes.length; i++) { if (table.childNodes[i] === prevNode) { magicNumber = i; } } } if (table === svg) { break; } } conclusion.transform.baseVal[0].matrix.e += dx; if (magicNumber !== 0) { continue; } if (table === svg) { break; // last step } const lineBelow = table.children[2] as SVGGraphicsElement; let lineStart = 0; if (lineBelow) { const offset1 = lineBelow.getTransformToElement(conclusion); lineStart = -offset1.e; const x1 = Number(lineBelow.getAttribute("x1")); const x2 = Number(lineBelow.getAttribute("x2")); lineBelow.setAttribute("x1", String(x1 + lineStart)); lineBelow.setAttribute("x2", String(x2 + lineStart)); } const label = table.parentElement!.children[1] as SVGGraphicsElement; if (label && label.transform) { label.transform.baseVal[0].matrix.e += lineStart; } } else { let left = null; let i = 0; for (const rawNode of row.children) { const node = rawNode as SVGGraphicsElement; if (i === 1 || i === 3) { i += 1; continue; // spacing node } const bbox = node.getBBox(); const mat = node.transform.baseVal[0]; if (mat) { bbox.x += mat.matrix.e; } // move box, and add padding between inference steps if (left == null) { // first box left = bbox.x + bbox.width; } else { // this box has some elements left of it // -> move to free space after other elements mat.matrix.e -= bbox.x - left - padding; left = bbox.x + mat.matrix.e + bbox.width; } if (i == 2) { let parentNode = node.parentNode! as SVGGraphicsElement; while (parentNode.getAttribute("semantics") !== "bspr_inferenceRule:down") { parentNode = parentNode.parentNode! as SVGGraphicsElement; } parentNode = parentNode.children[2] as SVGGraphicsElement; const rule = node.querySelector(inferenceRuleSelector); if (rule) { // this selector should be checked again when updating MathJax const term = rule.children[1].children[0].children[0].children[1].children[0] as SVGGraphicsElement; let w = -parentNode.getTransformToElement(term).e; w += term.getBBox().width; w += padding; parentNode.setAttribute("x2", w.toString()); } } i += 1; } } } const conclusion0 = svg.querySelector(inferenceRuleSelector)!.children[1].children[0].children[0].children[1] as SVGGraphicsElement; const conclusionWidth = conclusion0.getBBox().width; const svgWidth = svg.viewBox.baseVal.width; const offset = (svg.children[1] as SVGGraphicsElement).getTransformToElement(conclusion0); (svg.children[1] as SVGGraphicsElement).transform.baseVal[0].matrix.e += offset.e + svgWidth / 2 - conclusionWidth / 2; console.timeEnd('stepCalculation'); if (nodeIterator.length >= 3) { // should not be used on empty SVGs window.svgPanZoomFun(svg, { fit: false, controlIconsEnabled: true, customEventsHandler: { // Halt all touch events haltEventListeners: ['touchstart', 'touchend', 'touchmove', 'touchleave', 'touchcancel'], // Init custom events handler init: function(options) { const instance = options.instance; // Init Hammer // @ts-ignore this.hammer = Hammer(options.svgElement); // @ts-ignore this.hammer.get('pinch').set({enable: true}); // Handle double tap // @ts-ignore this.hammer.on('doubletap', () => { options.instance.zoomIn() }); let pannedX = 0; let pannedY = 0; // Handle pan // @ts-ignore this.hammer.on('panstart panmove', ev => { // On pan start reset panned variables if (ev.type === 'panstart') { pannedX = 0 pannedY = 0 } // Pan only the difference instance.panBy({x: ev.deltaX - pannedX, y: ev.deltaY - pannedY}) pannedX = ev.deltaX pannedY = ev.deltaY }); let initialScale = 1; // Handle pinch // @ts-ignore this.hammer.on('pinchstart pinchmove', function(ev){ // On pinch start remember initial zoom if (ev.type === 'pinchstart') { initialScale = instance.getZoom() instance.zoomAtPoint(initialScale * ev.scale, {x: ev.center.x, y: ev.center.y}) } instance.zoomAtPoint(initialScale * ev.scale, {x: ev.center.x, y: ev.center.y}) }); // Prevent moving the page on some devices when panning over SVG options.svgElement.addEventListener('touchmove', function(e: TouchEvent){ e.preventDefault(); }); } // Destroy custom events handler , destroy: function(){ // @ts-ignore this.hammer.destroy() } } }); // add tooltips to buttons const zoomIn = document.createElementNS("http://www.w3.org/2000/svg", "title"); zoomIn.append(document.createTextNode("zoom in")); svg.getElementById("svg-pan-zoom-zoom-in")!.children[0].appendChild(zoomIn); const zoomOut = document.createElementNS("http://www.w3.org/2000/svg", "title"); zoomOut.append(document.createTextNode("zoom out")); svg.getElementById("svg-pan-zoom-zoom-out")!.appendChild(zoomOut); // move control to upper left corner let matrix = svg.getElementById("svg-pan-zoom-controls")!.transform.baseVal[0].matrix; matrix.e = 0; matrix.f = 0; } this.steps = steps; this.showStep(0); this.$server!.setStepCount(steps.length); } } } customElements.define('tc-proof-tree', MathjaxProofTree);