diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index 984404c..55a03c3 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/frontend/src/mathjax-proof-tree.ts @@ -8,9 +8,11 @@ declare global { interface SVGElement { viewBox: SVGAnimatedRect; } + interface SVGGraphicsElement { getTransformToElement: (other: SVGGraphicsElement) => SVGMatrix; } + interface SVGTransformList { [index: number]: SVGTransform; } @@ -60,32 +62,6 @@ class MathjaxProofTree extends MathjaxAdapter { stepIdx++; } } - // then fix some mathjax layout issues - for (const step of root.querySelectorAll(stepSelector)) { - const infRule = step.querySelector(inferenceRuleSelector); - if (infRule === null || infRule.children.length != 3) { - continue; - } - const stepAbove = infRule.children[0] as SVGGraphicsElement; - const infRuleAbove = stepAbove.querySelector(inferenceRuleSelector)!; - if (infRuleAbove === null || infRuleAbove.children.length != 3) { - continue; - } - let termAbove = infRuleAbove.children[1] as SVGGraphicsElement; - let dx = termAbove.getBBox().x; - termAbove = termAbove.parentElement as HTMLElement & SVGGraphicsElement; - while (termAbove.parentElement!.getAttribute("semantics") !== "bspr_inferenceRule:down") { - if (termAbove.transform.baseVal !== null) { - if (termAbove.transform.baseVal.numberOfItems !== 1) { - termAbove = termAbove.parentElement as HTMLElement & SVGGraphicsElement; - continue; - } - dx += termAbove.transform.baseVal[0].matrix.e; - termAbove = termAbove.parentElement as HTMLElement & SVGGraphicsElement; - } - } - stepAbove.transform.baseVal[0].matrix.e -= dx; - } // then create the steps let steps: [SVGElement, SVGElement[]][] = []; stepIdx = 0; @@ -137,24 +113,61 @@ class MathjaxProofTree extends MathjaxAdapter { // 2. place inference conclusions under the center of their line const svg = root.querySelector("svg")!; svg.viewBox.baseVal.width = Math.min(100000, svg.viewBox.baseVal.width); - let counter = 0; - let oldWidth = NaN; - let newWidth = (svg.children[1] as SVGGraphicsElement).getBBox().width; - // rendering LaTeX often requires multiple passes over the input.. - let iterations = 0; - let extraIterations = 1; - while (isNaN(oldWidth) || Math.abs(oldWidth - newWidth) > 5000 || extraIterations > 0) { - if (!(isNaN(oldWidth) || Math.abs(oldWidth - newWidth) > 5000)) { - extraIterations--; - } - iterations++; - oldWidth = newWidth; - const nodeIterator2 = [...svg.querySelectorAll("g[data-mml-node='mtr']")]; - // start layout fixes in the innermost part of the SVG - nodeIterator2.reverse(); - counter = 0; - for (const row of nodeIterator2) { - counter++; + + 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) { @@ -197,41 +210,6 @@ class MathjaxProofTree extends MathjaxAdapter { i += 1; } } - const nodeIterator1 = [...svg.querySelectorAll(inferenceRuleSelector)]; - // start layout fixes in the innermost part of the SVG - nodeIterator1.reverse(); - for (const rule of nodeIterator1) { - const conclusion = rule.children[1].querySelector('g[data-mml-node="mstyle"]')!; - const conclusionBox = conclusion.getBBox(); - const line = rule.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 = rule.parentNode as SVGGraphicsElement; - while (table.getAttribute("semantics") !== "bspr_inferenceRule:down") { - table = table.parentNode as SVGGraphicsElement; - if (table === svg) { - break; - } - } - conclusion.transform.baseVal[0].matrix.e += dx; - if (table === svg) { - break; // last step - } - const lineBelow = table.children[2] as SVGGraphicsElement; - if (lineBelow) { - const x1 = Number(lineBelow.getAttribute("x1")); - const x2 = Number(lineBelow.getAttribute("x2")); - lineBelow.setAttribute("x1", String(x1 + dx)); - lineBelow.setAttribute("x2", String(x2 + dx)); - } - const label = table.parentElement!.children[1] as SVGGraphicsElement; - if (label && label.transform) { - label.transform.baseVal[0].matrix.e += dx; - } - } - newWidth = (svg.children[1] as SVGGraphicsElement).getBBox().width; } const conclusion0 = svg.querySelector(inferenceRuleSelector)!.children[1].children[0].children[0].children[1] as SVGGraphicsElement; const conclusionWidth = conclusion0.getBBox().width; @@ -239,9 +217,8 @@ class MathjaxProofTree extends MathjaxAdapter { 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'); - console.log("Iterations: " + iterations); - if (counter >= 3) { + if (nodeIterator.length >= 3) { // should not be used on empty SVGs window.svgPanZoomFun(svg, { fit: false }); } diff --git a/src/test/java/edu/kit/typicalc/view/ScreenshotIT.java b/src/test/java/edu/kit/typicalc/view/ScreenshotIT.java index 2c31a17..6c9a516 100644 --- a/src/test/java/edu/kit/typicalc/view/ScreenshotIT.java +++ b/src/test/java/edu/kit/typicalc/view/ScreenshotIT.java @@ -190,4 +190,35 @@ public class ScreenshotIT extends AbstractIT { assertTrue("Screenshot comparison for 'exportLatexWithAssumptions' (stage 3) failed", testBench().compareScreen("exportLatexWithAssumptions3")); } + + @Test + public void testScenario1() throws IOException { + InputBarElement inputBar = $(InputBarElement.class).first(); + String term = "λx. f x"; + inputBar.setCurrentValue(term); + + // check if the correct term is entered + Assert.assertEquals(term, inputBar.getCurrentValue()); + inputBar.typeInfer(); + + ControlPanelElement controlPanelElement = $(ControlPanelElement.class).first(); + + assertTrue(testBench().compareScreen("testScenario1_step0")); + controlPanelElement.nextStep(); + assertTrue(testBench().compareScreen("testScenario1_step1")); + controlPanelElement.nextStep(); + assertTrue(testBench().compareScreen("testScenario1_step2")); + controlPanelElement.nextStep(); + assertTrue(testBench().compareScreen("testScenario1_step3")); + controlPanelElement.nextStep(); + assertTrue(testBench().compareScreen("testScenario1_step4")); + controlPanelElement.previousStep(); + assertTrue(testBench().compareScreen("testScenario1_step3")); + controlPanelElement.previousStep(); + assertTrue(testBench().compareScreen("testScenario1_step2")); + controlPanelElement.firstStep(); + assertTrue(testBench().compareScreen("testScenario1_step0")); + controlPanelElement.lastStep(); + assertTrue(testBench().compareScreen("testScenario1_step4gi")); + } } diff --git a/src/test/java/edu/kit/typicalc/view/pageobjects/ControlPanelElement.java b/src/test/java/edu/kit/typicalc/view/pageobjects/ControlPanelElement.java index 285d455..43180f3 100644 --- a/src/test/java/edu/kit/typicalc/view/pageobjects/ControlPanelElement.java +++ b/src/test/java/edu/kit/typicalc/view/pageobjects/ControlPanelElement.java @@ -6,7 +6,19 @@ import com.vaadin.testbench.annotations.Attribute; @Attribute(name = "id", value = "control-panel") public class ControlPanelElement extends HorizontalLayoutElement { - + + public void firstStep() { + $(ButtonElement.class).get(1).click(); + } + + public void previousStep() { + $(ButtonElement.class).get(2).click(); + } + + public void nextStep() { + $(ButtonElement.class).get(3).click(); + } + public void lastStep() { $(ButtonElement.class).get(4).click(); } diff --git a/src/test/resources/screenshots/testScenario1_step0_linux_firefox_86.png b/src/test/resources/screenshots/testScenario1_step0_linux_firefox_86.png new file mode 100644 index 0000000..21697f3 Binary files /dev/null and b/src/test/resources/screenshots/testScenario1_step0_linux_firefox_86.png differ diff --git a/src/test/resources/screenshots/testScenario1_step1_linux_firefox_86.png b/src/test/resources/screenshots/testScenario1_step1_linux_firefox_86.png new file mode 100644 index 0000000..36beb02 Binary files /dev/null and b/src/test/resources/screenshots/testScenario1_step1_linux_firefox_86.png differ diff --git a/src/test/resources/screenshots/testScenario1_step2_linux_firefox_86.png b/src/test/resources/screenshots/testScenario1_step2_linux_firefox_86.png new file mode 100644 index 0000000..e5cf82a Binary files /dev/null and b/src/test/resources/screenshots/testScenario1_step2_linux_firefox_86.png differ diff --git a/src/test/resources/screenshots/testScenario1_step3_linux_firefox_86.png b/src/test/resources/screenshots/testScenario1_step3_linux_firefox_86.png new file mode 100644 index 0000000..8e3ef5c Binary files /dev/null and b/src/test/resources/screenshots/testScenario1_step3_linux_firefox_86.png differ diff --git a/src/test/resources/screenshots/testScenario1_step4_linux_firefox_86.png b/src/test/resources/screenshots/testScenario1_step4_linux_firefox_86.png new file mode 100644 index 0000000..234dc36 Binary files /dev/null and b/src/test/resources/screenshots/testScenario1_step4_linux_firefox_86.png differ