From 35013bd81915409d1c79c27aa99c749dedc56c96 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Mon, 19 Jul 2021 11:21:54 +0200
Subject: [PATCH] Show correct tooltips for polymorphic steps

fixes #16
---
 frontend/src/mathjax-setup.js                              | 3 ++-
 .../content/typeinferencecontent/MathjaxProofTree.java     | 6 ++++++
 .../typeinferencecontent/latexcreator/LatexCreator.java    | 7 +++----
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/frontend/src/mathjax-setup.js b/frontend/src/mathjax-setup.js
index 586c1ee..3f71e0e 100644
--- a/frontend/src/mathjax-setup.js
+++ b/frontend/src/mathjax-setup.js
@@ -135,7 +135,8 @@ window.MathJax = {
                         .typicalc-type, g[semantics='bspr_prooflabel:left'] {\
                             stroke: transparent; stroke-width: 600px; pointer-events: all;\
                         }\
-                        #typicalc-definition-abs, #typicalc-definition-app, #typicalc-definition-const, #typicalc-definition-var, #typicalc-definition-let {\
+                        #typicalc-definition-abs, #typicalc-definition-abs-let, #typicalc-definition-app,\
+                        #typicalc-definition-const, #typicalc-definition-var, #typicalc-definition-var-let, #typicalc-definition-let {\
                             display: none;\
                             border: 2px solid red;\
                         }";
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java
index 90bfdb7..b9c2240 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java
@@ -36,6 +36,9 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
                 + "\\cssId{typicalc-definition-abs}{"
                 + getTranslation("root.absLatex")
                 + "}"
+                + "\\cssId{typicalc-definition-abs-let}{"
+                + getTranslation("root.absLetLatex")
+                + "}"
                 + "\\cssId{typicalc-definition-app}{"
                 + getTranslation("root.appLatex")
                 + "}"
@@ -45,6 +48,9 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
                 + "\\cssId{typicalc-definition-var}{"
                 + getTranslation("root.varLatex")
                 + "}"
+                + "\\cssId{typicalc-definition-var-let}{"
+                + getTranslation("root.varLetLatex")
+                + "}"
                 + "\\cssId{typicalc-definition-let}{"
                 + getTranslation("root.letLatex")
                 + "}"
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
index 59bdb1b..4483864 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
@@ -126,8 +126,8 @@ public class LatexCreator implements StepVisitor {
     public void visit(AbsStepWithLet absL) {
         tree.insert(0, generateConclusion(absL,
                 mode == LatexCreatorMode.MATHJAX
-                        ? "\\LeftLabel{\\class{typicalc-label typicalc-label-abs typicalc-step-" + absL.getStepIndex()
-                                + "}{\\textrm A{\\small BS}}}" : LABEL_ABS, // TODO: differentiate with let
+                        ? "\\LeftLabel{\\class{typicalc-label typicalc-label-abs-let typicalc-step-" + absL.getStepIndex()
+                                + "}{\\textrm A{\\small BS}}}" : LABEL_ABS,
                 UIC));
         absL.getPremise().accept(this);
     }
@@ -174,9 +174,8 @@ public class LatexCreator implements StepVisitor {
     public void visit(VarStepWithLet varL) {
         String latex = "";
         if (mode == LatexCreatorMode.MATHJAX) {
-            latex = "\\LeftLabel{\\class{typicalc-label typicalc-label-var "
+            latex = "\\LeftLabel{\\class{typicalc-label typicalc-label-var-let "
                     + "typicalc-step-" + varL.getStepIndex() + "}{\\textrm V{\\small AR}}}";
-            // TODO: differentiate with let
         } else {
             latex = LABEL_VAR;
         }