From ed9cb6a3fae1d9d1871312be566bb2b1ec13f003 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Thu, 7 Oct 2021 11:03:39 +0200
Subject: [PATCH] Fix type highlighting when switching language

---
 frontend/src/mathjax-proof-tree.ts | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts
index 0ce2457..8c64f7a 100644
--- a/frontend/src/mathjax-proof-tree.ts
+++ b/frontend/src/mathjax-proof-tree.ts
@@ -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) {