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

Display premises always, space between premises

Browse Source
This commit is contained in:
Arne Keller 2021-02-03 21:43:40 +01:00
parent 2930a274ed
commit 84a9a3c5a4
2 changed files with 64 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -11,33 +11,84 @@ class MathjaxProofTree extends MathjaxAdapter {
protected showStep(n: number): void {
for (let current = 0; current < this.steps.length; current++) {
if (current <= n) {
this.steps[current].style.display = "";
} else {
this.steps[current].style.display = "none";
this.steps[current][0].style.display = "none";
for (const node of this.steps[current][1]) {
node.style.display = "none";
}
}
for (let current = 0; current <= n; current++) {
this.steps[current][0].style.display = "";
for (const node of this.steps[current][1]) {
node.style.display = "";
}
}
}
protected calculateSteps(): void {
if (this.shadowRoot !== null) {
// first, enumerate all of the steps
let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
let steps = [];
let a = null;
while (a = nodeIterator.nextNode()) {
// todo remove @ts suppress
// @ts-ignore
let stepIdx = 0;
while (a = nodeIterator.nextNode() as HTMLElement) {
let semantics = a.getAttribute("semantics");
if (semantics == null || a.nodeName !== "g") {
continue;
}
if (semantics.startsWith("bspr_inference:") || semantics.startsWith("bspr_axiom")) {
steps.push(a);
// @ts-ignore
a.setAttribute("typicalc", "step");
a.setAttribute("id", "step" + stepIdx);
stepIdx++;
}
}
// then create the steps
nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
steps = [];
a = null;
stepIdx = 0;
while (a = nodeIterator.nextNode() as HTMLElement) {
let semantics = a.getAttribute("semantics");
if (semantics == null || a.nodeName !== "g") {
continue;
}
if (semantics.startsWith("bspr_inference:") || semantics.startsWith("bspr_axiom")) {
const id = "step" + stepIdx;
stepIdx++;
// find the next one/two steps above this one
const aboveStep1 = a.querySelector<HTMLElement>("#" + id + " g[typicalc=\"step\"]");
let above = [];
if (aboveStep1 != null) {
const parent = aboveStep1.parentNode!.parentNode! as HTMLElement;
parent.setAttribute("id", "typicalc-selector");
for (const node of parent.querySelectorAll("#typicalc-selector > g > g[typicalc=\"step\"")) {
above.push(node as HTMLElement);
}
parent.removeAttribute("id");
}
const rule = a.querySelector("#" + id + " g[semantics=\"bspr_inferenceRule:down\"]");
if (rule !== null) {
let i = 0;
for (const node of rule.childNodes) {
if (i !== 1) {
above.push(node);
}
i += 1;
}
}
const label = a.querySelector("#" + id +" g[semantics=\"bspr_prooflabel:left\"]");
if (label !== null) {
const labelElement = label as HTMLElement;
labelElement.style.display = "none";
above.push(labelElement);
}
if (!semantics.startsWith("bspr_axiom")) {
steps.push([a, above]);
}
a.style.display = "none";
}
}
// @ts-ignore
this.steps = steps;
this.showStep(0);
// @ts-ignore
@ -46,4 +97,4 @@ class MathjaxProofTree extends MathjaxAdapter {
}
}
customElements.define('tc-proof-tree', MathjaxProofTree);
customElements.define('tc-proof-tree', MathjaxProofTree);

3
frontend/src/mathjax-setup.js
View File

@ -130,7 +130,8 @@ mjx-container {\
if (left == null) {
left = bbox.x + bbox.width;
} else {
mat.matrix.e -= bbox.x - left;
// 500 space between inference steps
mat.matrix.e -= bbox.x - left - 500;
left = bbox.x + mat.matrix.e + bbox.width;
}
i += 1;