Semantic highlighting of variables

This commit is contained in:
Arne Keller 2021-07-02 14:57:25 +02:00
parent 30b14a2e1a
commit 480275e3a7
2 changed files with 7 additions and 2 deletions

View File

@ -4,6 +4,7 @@ import edu.kit.typicalc.model.parser.LambdaParser;
import edu.kit.typicalc.model.parser.ParseError; import edu.kit.typicalc.model.parser.ParseError;
import edu.kit.typicalc.model.parser.TypeAssumptionParser; import edu.kit.typicalc.model.parser.TypeAssumptionParser;
import edu.kit.typicalc.model.term.LambdaTerm; 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.term.VarTerm;
import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeAbstraction;
import edu.kit.typicalc.util.Result; import edu.kit.typicalc.util.Result;
@ -39,8 +40,10 @@ public class ModelImpl implements Model {
if (assumptionMap.isError()) { if (assumptionMap.isError()) {
return new Result<>(null, assumptionMap.unwrapError()); return new Result<>(null, assumptionMap.unwrapError());
} }
//Create and return TypeInferer // scope variables
TypeInferer typeInferer = new TypeInferer(result.unwrap(), assumptionMap.unwrap()); LambdaTerm term = result.unwrap();
term.accept(new ScopingVisitor());
TypeInferer typeInferer = new TypeInferer(term, assumptionMap.unwrap());
return new Result<>(typeInferer, null); return new Result<>(typeInferer, null);
} }
} }

View File

@ -82,6 +82,8 @@ public class LatexCreatorTerm implements TermVisitor {
if (mode == LatexCreatorMode.MATHJAX) { if (mode == LatexCreatorMode.MATHJAX) {
latex.append("\\class{typicalc-type typicalc-type-v-"); latex.append("\\class{typicalc-type typicalc-type-v-");
latex.append(varTerm.hashCode()); latex.append(varTerm.hashCode());
latex.append("-");
latex.append(varTerm.uniqueIndex());
latex.append("}{"); latex.append("}{");
} }
latex.append(MONO_TEXT); latex.append(MONO_TEXT);