arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-12 20:23:52 +00:00
Code Issues Packages Projects Releases Wiki Activity

Final var step: show premise in second step

Browse Source
This commit is contained in:
Arne Keller 2021-02-04 21:17:03 +01:00
parent bdabb010b0
commit e1a90b3923
1 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -26,6 +26,7 @@ class MathjaxProofTree extends MathjaxAdapter {
protected calculateSteps(): void { protected calculateSteps(): void {
if (this.shadowRoot !== null) { if (this.shadowRoot !== null) {
let semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
// first, enumerate all of the steps // first, enumerate all of the steps
let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT); let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
let steps = []; let steps = [];
@ -36,7 +37,7 @@ class MathjaxProofTree extends MathjaxAdapter {
if (semantics == null || a.nodeName !== "g") { if (semantics == null || a.nodeName !== "g") {
continue; continue;
} }
if (semantics.startsWith("bspr_inference:") || semantics.startsWith("bspr_axiom")) { if (semanticsMatch(semantics)) {
a.setAttribute("typicalc", "step"); a.setAttribute("typicalc", "step");
a.setAttribute("id", "step" + stepIdx); a.setAttribute("id", "step" + stepIdx);
stepIdx++; stepIdx++;
@ -86,7 +87,7 @@ class MathjaxProofTree extends MathjaxAdapter {
if (semantics == null || a.nodeName !== "g") { if (semantics == null || a.nodeName !== "g") {
continue; continue;
} }
if (semantics.startsWith("bspr_inference:") || semantics.startsWith("bspr_axiom")) { if (semanticsMatch(semantics)) {
const id = "step" + stepIdx; const id = "step" + stepIdx;
stepIdx++; stepIdx++;
@ -102,6 +103,7 @@ class MathjaxProofTree extends MathjaxAdapter {
parent.removeAttribute("id"); parent.removeAttribute("id");
} }
const rule = a.querySelector("#" + id + " g[semantics=\"bspr_inferenceRule:down\"]"); const rule = a.querySelector("#" + id + " g[semantics=\"bspr_inferenceRule:down\"]");
console.log(rule);
if (rule !== null) { if (rule !== null) {
let i = 0; let i = 0;
for (const node of rule.childNodes) { for (const node of rule.childNodes) {
@ -114,17 +116,13 @@ class MathjaxProofTree extends MathjaxAdapter {
const label = a.querySelector("#" + id +" g[semantics=\"bspr_prooflabel:left\"]"); const label = a.querySelector("#" + id +" g[semantics=\"bspr_prooflabel:left\"]");
if (label !== null) { if (label !== null) {
const labelElement = label as HTMLElement; const labelElement = label as HTMLElement;
//labelElement.style.display = "none";
above.push(labelElement); above.push(labelElement);
} }
if (stepIdx === 1) { if (stepIdx === 1) {
steps.push([a, []]); steps.push([a, []]);
} }
if (!semantics.startsWith("bspr_axiom")) {
steps.push([a, above]); steps.push([a, above]);
} }
//a.style.display = "none";
}
} }
const svg = this.shadowRoot.querySelector<SVGElement>("svg")!; const svg = this.shadowRoot.querySelector<SVGElement>("svg")!;
const nodeIterator2 = svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']"); const nodeIterator2 = svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']");