mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
Optimize frontend script and style
This commit is contained in:
parent
49adac2a88
commit
91daed42c4
@ -304,14 +304,9 @@ class MathjaxProofTree extends MathjaxAdapter {
|
|||||||
if (explainer) {
|
if (explainer) {
|
||||||
const ctm1 = svg.getBoundingClientRect();
|
const ctm1 = svg.getBoundingClientRect();
|
||||||
const ctm2 = this.defElBackground!.getBoundingClientRect();
|
const ctm2 = this.defElBackground!.getBoundingClientRect();
|
||||||
explainer.style.left = (ctm2.left - ctm1.left) + "px";
|
|
||||||
explainer.style.top = (ctm2.bottom - ctm1.top) + "px";
|
|
||||||
// TODO(performance): this should be more efficient, but somehow flickers
|
|
||||||
/*
|
|
||||||
const dx = (ctm2.left - ctm1.left) - explainer.offsetLeft;
|
const dx = (ctm2.left - ctm1.left) - explainer.offsetLeft;
|
||||||
const dy = (ctm2.bottom - ctm1.top) - explainer.offsetTop;
|
const dy = (ctm2.bottom - ctm1.top) - explainer.offsetTop;
|
||||||
explainer.style.transform = "translate(" + dx + "px," + dy + "px)";
|
explainer.style.transform = "translate(" + dx + "px," + dy + "px)";
|
||||||
*/
|
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
// @ts-ignore
|
// @ts-ignore
|
||||||
@ -569,7 +564,11 @@ class MathjaxProofTree extends MathjaxAdapter {
|
|||||||
}
|
}
|
||||||
this.shadowRoot!
|
this.shadowRoot!
|
||||||
.querySelectorAll<SVGGraphicsElement>(".typicalc-definition")!
|
.querySelectorAll<SVGGraphicsElement>(".typicalc-definition")!
|
||||||
.forEach((it) => it.style.display = "none");
|
.forEach((it) => {
|
||||||
|
if (it.style) {
|
||||||
|
it.style.display = "none"
|
||||||
|
}
|
||||||
|
});
|
||||||
let defElBackground = this.shadowRoot!.getElementById(this.hoverTextBackgroundElID);
|
let defElBackground = this.shadowRoot!.getElementById(this.hoverTextBackgroundElID);
|
||||||
if (defElBackground) {
|
if (defElBackground) {
|
||||||
defElBackground.parentElement!.removeChild(defElBackground);
|
defElBackground.parentElement!.removeChild(defElBackground);
|
||||||
|
@ -20,6 +20,8 @@
|
|||||||
|
|
||||||
#input-bar {
|
#input-bar {
|
||||||
width: 75%;
|
width: 75%;
|
||||||
|
/* require a larger width on small screens! */
|
||||||
|
min-width: min(100%, 1100px);
|
||||||
flex-grow: 1;
|
flex-grow: 1;
|
||||||
align-items: flex-end;
|
align-items: flex-end;
|
||||||
padding: 0 1em;
|
padding: 0 1em;
|
||||||
|
Loading…
Reference in New Issue
Block a user