From 480275e3a7cff6a19dfef2d5fa014641da89a734 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Fri, 2 Jul 2021 14:57:25 +0200
Subject: [PATCH] Semantic highlighting of variables

---
 src/main/java/edu/kit/typicalc/model/ModelImpl.java        | 7 +++++--
 .../latexcreator/LatexCreatorTerm.java                     | 2 ++
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/model/ModelImpl.java b/src/main/java/edu/kit/typicalc/model/ModelImpl.java
index a1fbd28..d2472a7 100644
--- a/src/main/java/edu/kit/typicalc/model/ModelImpl.java
+++ b/src/main/java/edu/kit/typicalc/model/ModelImpl.java
@@ -4,6 +4,7 @@ import edu.kit.typicalc.model.parser.LambdaParser;
 import edu.kit.typicalc.model.parser.ParseError;
 import edu.kit.typicalc.model.parser.TypeAssumptionParser;
 import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.ScopingVisitor;
 import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 import edu.kit.typicalc.util.Result;
@@ -39,8 +40,10 @@ public class ModelImpl implements Model {
         if (assumptionMap.isError()) {
             return new Result<>(null, assumptionMap.unwrapError());
         }
-        //Create and return TypeInferer
-        TypeInferer typeInferer = new TypeInferer(result.unwrap(), assumptionMap.unwrap());
+        // scope variables
+        LambdaTerm term = result.unwrap();
+        term.accept(new ScopingVisitor());
+        TypeInferer typeInferer = new TypeInferer(term, assumptionMap.unwrap());
         return new Result<>(typeInferer, null);
     }
 }
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java
index b943d54..4d2f684 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java
@@ -82,6 +82,8 @@ public class LatexCreatorTerm implements TermVisitor {
         if (mode == LatexCreatorMode.MATHJAX) {
             latex.append("\\class{typicalc-type typicalc-type-v-");
             latex.append(varTerm.hashCode());
+            latex.append("-");
+            latex.append(varTerm.uniqueIndex());
             latex.append("}{");
         }
         latex.append(MONO_TEXT);