Move hidden tooltip background off useful area

This commit is contained in:
Arne Keller 2021-08-10 11:45:40 +02:00
parent 90833c37b5
commit 9773385eab

View File

@ -492,7 +492,7 @@ class MathjaxProofTree extends MathjaxAdapter {
const defId = typeTarget.classList[1].replace("-label-", "-definition-"); const defId = typeTarget.classList[1].replace("-label-", "-definition-");
this.shadowRoot!.getElementById(defId)!.style.display = "none"; this.shadowRoot!.getElementById(defId)!.style.display = "none";
let defElBackground = this.shadowRoot!.getElementById(defId + "-background"); let defElBackground = this.shadowRoot!.getElementById(defId + "-background");
defElBackground!.setAttribute("y", String(10000)); defElBackground!.setAttribute("y", String(-10000));
defElBackground!.setAttribute("fill", "transparent"); defElBackground!.setAttribute("fill", "transparent");
if (typeTarget.classList.length >= 3) { if (typeTarget.classList.length >= 3) {
hoverStylesUnification!.innerHTML = ""; hoverStylesUnification!.innerHTML = "";