This commit is contained in:
Arne Keller 2021-11-29 15:49:55 +01:00
parent cfb27e3de3
commit da87576326
2 changed files with 7 additions and 5 deletions

View File

@ -79,10 +79,11 @@ class MathjaxProofTree extends MathjaxAdapter {
console.time('stepCalculation');
const svg = this.shadowRoot!.querySelector<SVGElement>("svg")!;
let root = this.shadowRoot!.querySelector("#typicalc-prooftree")! as SVGElement;
let root = this.shadowRoot!.querySelector("#typicalc-prooftree") as SVGElement || this.shadowRoot!.querySelector("semantics") as SVGElement;
while (!root.getAttribute("semantics")) {
root = root.parentNode! as SVGElement;
}
root.id = "typicalc-prooftree";
// first, enumerate all of the steps
// and assign IDs
let stepIdx = 0;
@ -140,8 +141,8 @@ class MathjaxProofTree extends MathjaxAdapter {
svg.viewBox.baseVal.width = Math.min(50000, svg.viewBox.baseVal.width);
svg.viewBox.baseVal.width = Math.max(20000, svg.viewBox.baseVal.width);
// center on first visible element
const finalConclusion = svg
.querySelector<SVGGraphicsElement>("#typicalc-prooftree > g[semantics='bspr_inferenceRule:down']")!
const finalConclusion = root
.querySelector<SVGGraphicsElement>("g[semantics='bspr_inferenceRule:down']")!
.children[1]! as SVGGraphicsElement;
const conclusionBBox = finalConclusion.getBBox();
const mainGroupElement = svg.children[1]! as SVGGraphicsElement;

View File

@ -36,7 +36,7 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
*/
public MathjaxProofTree(String latex, List<String> extraData) {
// step definitions used for tooltips
content.add("\\[\\cssId{typicalc-prooftree}{" + latex + "}"
String latexCode = "\\[\\cssId{typicalc-prooftree}{" + latex + "}"
+ "\\class{typicalc-definition}{"
+ "\\cssId{typicalc-definition-abs}{"
+ getTranslation("root.absLatex")
@ -72,7 +72,8 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
+ getTranslation("root.letLatex")
+ "}"
+ "}"
+ "\\]");
+ "\\]";
content.add(latexCode);
getElement().callJsFunction("requestTypeset", new Gson().toJson(extraData));
}