arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-09-16 16:55:08 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix type highlighting when switching language

Browse Source
This commit is contained in:
Arne Keller 2021-10-07 11:03:39 +02:00
parent 980b2d838d
commit ed9cb6a3fa
1 changed files with 13 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -392,13 +392,7 @@ class MathjaxProofTree extends MathjaxAdapter {
this.hoverStyles.id = "typicalc-hover-styles";
root.querySelector("mjx-head")!.appendChild(this.hoverStyles);
}
const unificationEl = root.host.parentElement!.parentElement!.querySelector("tc-unification")!;
this.hoverStylesUnification = unificationEl.shadowRoot!.querySelector("#typicalc-hover-styles");
if (!this.hoverStylesUnification) {
this.hoverStylesUnification = document.createElement('style');
this.hoverStylesUnification.id = "typicalc-hover-styles";
unificationEl.shadowRoot!.querySelector("mjx-head")!.appendChild(this.hoverStylesUnification);
}
this.setupUnificationStyles();
// set the size of the rendered SVG to the size of the container element
if (!root.querySelector("#style-fixes")) {
const style = document.createElement('style');
@ -449,6 +443,7 @@ class MathjaxProofTree extends MathjaxAdapter {
const typeClass = typeTarget.classList[1];
const css = "." + typeClass + " { color: red; }";
this.hoverStyles!.innerHTML = css;
this.setupUnificationStyles();
this.hoverStylesUnification!.innerHTML = css;
} else if (isLabel) {
let stepTarget = typeTarget;
@ -558,6 +553,17 @@ class MathjaxProofTree extends MathjaxAdapter {
this.$server!.setStepCount(this.steps.length);
}
// creates the mirrored style document in the unification element
private setupUnificationStyles() {
const unificationEl = this.shadowRoot!.host.parentElement!.parentElement!.querySelector("tc-unification")!;
this.hoverStylesUnification = unificationEl.shadowRoot!.querySelector("#typicalc-hover-styles");
if (!this.hoverStylesUnification) {
this.hoverStylesUnification = document.createElement('style');
this.hoverStylesUnification.id = "typicalc-hover-styles";
unificationEl.shadowRoot!.querySelector("mjx-head")!.appendChild(this.hoverStylesUnification);
}
}
private destroyTooltip() {
const svg = this.shadowRoot!.querySelector<SVGElement>("svg");
if (!svg) {