arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-09 19:00:48 +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:
ucrhh 2021-02-27 22:21:38 +01:00
commit 66ad18fe93
1 changed files with 58 additions and 81 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -8,9 +8,11 @@ declare global {
interface SVGElement { interface SVGElement {
viewBox: SVGAnimatedRect; viewBox: SVGAnimatedRect;
} }
interface SVGGraphicsElement { interface SVGGraphicsElement {
getTransformToElement: (other: SVGGraphicsElement) => SVGMatrix; getTransformToElement: (other: SVGGraphicsElement) => SVGMatrix;
} }
interface SVGTransformList { interface SVGTransformList {
[index: number]: SVGTransform; [index: number]: SVGTransform;
} }
@ -60,32 +62,6 @@ class MathjaxProofTree extends MathjaxAdapter {
stepIdx++; stepIdx++;
} }
} }
// then fix some mathjax layout issues
for (const step of root.querySelectorAll<SVGElement>(stepSelector)) {
const infRule = step.querySelector<SVGElement>(inferenceRuleSelector);
if (infRule === null || infRule.children.length != 3) {
continue;
}
const stepAbove = infRule.children[0] as SVGGraphicsElement;
const infRuleAbove = stepAbove.querySelector<HTMLElement>(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 // then create the steps
let steps: [SVGElement, SVGElement[]][] = []; let steps: [SVGElement, SVGElement[]][] = [];
stepIdx = 0; stepIdx = 0;
@ -137,24 +113,61 @@ class MathjaxProofTree extends MathjaxAdapter {
// 2. place inference conclusions under the center of their line // 2. place inference conclusions under the center of their line
const svg = root.querySelector<SVGElement>("svg")!; const svg = root.querySelector<SVGElement>("svg")!;
svg.viewBox.baseVal.width = Math.min(100000, svg.viewBox.baseVal.width); svg.viewBox.baseVal.width = Math.min(100000, svg.viewBox.baseVal.width);
let counter = 0;
let oldWidth = NaN; const nodeIterator = [...svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']," + inferenceRuleSelector)];
let newWidth = (svg.children[1] as SVGGraphicsElement).getBBox().width; console.log(`working with ${nodeIterator.length} nodes`);
// rendering LaTeX often requires multiple passes over the input.. // start layout fixes in the innermost part of the SVG
let iterations = 0; nodeIterator.reverse();
let extraIterations = 1; for (const row of nodeIterator) {
while (isNaN(oldWidth) || Math.abs(oldWidth - newWidth) > 5000 || extraIterations > 0) { const semantics = row.getAttribute("semantics");
if (!(isNaN(oldWidth) || Math.abs(oldWidth - newWidth) > 5000)) { if (semantics === "bspr_inferenceRule:down") {
extraIterations--; const conclusion = row.children[1].querySelector<SVGGraphicsElement>('g[data-mml-node="mstyle"]')!;
} const conclusionBox = conclusion.getBBox();
iterations++; const line = row.children[2] as SVGGraphicsElement;
oldWidth = newWidth; const bbox = line.getBBox();
const nodeIterator2 = [...svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']")];
// start layout fixes in the innermost part of the SVG const offset2 = line.getTransformToElement(conclusion);
nodeIterator2.reverse(); let dx = bbox.width / 2 + offset2.e - conclusionBox.width / 2;
counter = 0; dx += Number(line.getAttribute("x1"));
for (const row of nodeIterator2) { let table = row.parentNode as SVGGraphicsElement;
counter++; 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 left = null;
let i = 0; let i = 0;
for (const rawNode of row.children) { for (const rawNode of row.children) {
@ -197,41 +210,6 @@ class MathjaxProofTree extends MathjaxAdapter {
i += 1; i += 1;
} }
} }
const nodeIterator1 = [...svg.querySelectorAll<SVGGraphicsElement>(inferenceRuleSelector)];
// start layout fixes in the innermost part of the SVG
nodeIterator1.reverse();
for (const rule of nodeIterator1) {
const conclusion = rule.children[1].querySelector<SVGGraphicsElement>('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<SVGElement>(inferenceRuleSelector)!.children[1].children[0].children[0].children[1] as SVGGraphicsElement; const conclusion0 = svg.querySelector<SVGElement>(inferenceRuleSelector)!.children[1].children[0].children[0].children[1] as SVGGraphicsElement;
const conclusionWidth = conclusion0.getBBox().width; const conclusionWidth = conclusion0.getBBox().width;
@ -239,9 +217,8 @@ class MathjaxProofTree extends MathjaxAdapter {
const offset = (svg.children[1] as SVGGraphicsElement).getTransformToElement(conclusion0); 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; (svg.children[1] as SVGGraphicsElement).transform.baseVal[0].matrix.e += offset.e + svgWidth / 2 - conclusionWidth / 2;
console.timeEnd('stepCalculation'); console.timeEnd('stepCalculation');
console.log("Iterations: " + iterations);
if (counter >= 3) { if (nodeIterator.length >= 3) {
// should not be used on empty SVGs // should not be used on empty SVGs
window.svgPanZoomFun(svg, { fit: false }); window.svgPanZoomFun(svg, { fit: false });
} }