Fix layout of upper bar

This commit is contained in:
Arne Keller 2021-02-06 10:41:28 +01:00
parent c9512b57d2
commit 843430439d
3 changed files with 13 additions and 37 deletions

View File

@ -26,9 +26,10 @@ class MathjaxProofTree extends MathjaxAdapter {
protected calculateSteps(): void {
if (this.shadowRoot !== null) {
const root = this.shadowRoot;
let semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
// first, enumerate all of the steps
let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
let nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
let steps = [];
let a = null;
let stepIdx = 0;
@ -44,7 +45,7 @@ class MathjaxProofTree extends MathjaxAdapter {
}
}
// then fix some more mathjax layout issues
for (const step of this.shadowRoot.querySelectorAll<HTMLElement>('g[typicalc="step"]')) {
for (const step of root.querySelectorAll<HTMLElement>('g[typicalc="step"]')) {
const infRule = step.querySelector<HTMLElement>('g[semantics="bspr_inferenceRule:down"]');
if (infRule === null) {
continue;
@ -78,7 +79,7 @@ class MathjaxProofTree extends MathjaxAdapter {
stepAbove.transform.baseVal[0].matrix.e -= dx;
}
// then create the steps
nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
steps = [];
stepIdx = 0;
while (a = nodeIterator.nextNode() as HTMLElement) {
@ -122,7 +123,7 @@ class MathjaxProofTree extends MathjaxAdapter {
steps.push([a, above]);
}
}
const svg = this.shadowRoot.querySelector<SVGElement>("svg")!;
const svg = root.querySelector<SVGElement>("svg")!;
const nodeIterator2 = [...svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']")];
// start layout fixes in the innermost part of the SVG
nodeIterator2.reverse();
@ -170,8 +171,8 @@ class MathjaxProofTree extends MathjaxAdapter {
i += 1;
}
}
const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox();
// TODO: this does not work when using a permalink
const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox();
svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height);
if (counter >= 3) {
// should not be used on empty SVGs

View File

@ -1,13 +1,5 @@
@media (max-width: 500px) {
#inputField {
width: 20em;
}
}
@media (min-width: 1000px) {
#inputField {
width: 30em;
}
#inputField {
flex-grow: 1;
}
#inputField {
@ -16,6 +8,7 @@
#inputBar {
align-items: center;
padding: 1em;
}
vaadin-drawer-toggle {

View File

@ -19,31 +19,13 @@
}
#helpIcon {
margin-left: auto;
margin-left: 1em;
margin-right: 1em;
}
@media (max-width: 500px) {
#inputBar {
margin: auto;
}
#viewTitle {
margin-right: 5em;
}
}
@media (min-width: 1000px) {
#inputBar {
margin-left: 15em;
}
#viewTitle {
margin-right: auto;
}
#inputBar {
flex-grow: 1;
justify-content: end;
}