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

Show correct tooltips for polymorphic steps

Browse Source 
fixes #16
This commit is contained in:
Arne Keller 2021-07-19 11:21:54 +02:00
parent 08085ad44d
commit 35013bd819
3 changed files with 11 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
frontend/src/mathjax-setup.js
View File

@ -135,7 +135,8 @@ window.MathJax = {
.typicalc-type, g[semantics='bspr_prooflabel:left'] {\ .typicalc-type, g[semantics='bspr_prooflabel:left'] {\
stroke: transparent; stroke-width: 600px; pointer-events: all;\ 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;\ display: none;\
border: 2px solid red;\ border: 2px solid red;\
}"; }";

6
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java
View File

@ -36,6 +36,9 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
+ "\\cssId{typicalc-definition-abs}{" + "\\cssId{typicalc-definition-abs}{"
+ getTranslation("root.absLatex") + getTranslation("root.absLatex")
+ "}" + "}"
+ "\\cssId{typicalc-definition-abs-let}{"
+ getTranslation("root.absLetLatex")
+ "}"
+ "\\cssId{typicalc-definition-app}{" + "\\cssId{typicalc-definition-app}{"
+ getTranslation("root.appLatex") + getTranslation("root.appLatex")
+ "}" + "}"
@ -45,6 +48,9 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
+ "\\cssId{typicalc-definition-var}{" + "\\cssId{typicalc-definition-var}{"
+ getTranslation("root.varLatex") + getTranslation("root.varLatex")
+ "}" + "}"
+ "\\cssId{typicalc-definition-var-let}{"
+ getTranslation("root.varLetLatex")
+ "}"
+ "\\cssId{typicalc-definition-let}{" + "\\cssId{typicalc-definition-let}{"
+ getTranslation("root.letLatex") + getTranslation("root.letLatex")
+ "}" + "}"

7
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
View File

@ -126,8 +126,8 @@ public class LatexCreator implements StepVisitor {
public void visit(AbsStepWithLet absL) { public void visit(AbsStepWithLet absL) {
tree.insert(0, generateConclusion(absL, tree.insert(0, generateConclusion(absL,
mode == LatexCreatorMode.MATHJAX mode == LatexCreatorMode.MATHJAX
? "\\LeftLabel{\\class{typicalc-label typicalc-label-abs typicalc-step-" + absL.getStepIndex() ? "\\LeftLabel{\\class{typicalc-label typicalc-label-abs-let typicalc-step-" + absL.getStepIndex()
+ "}{\\textrm A{\\small BS}}}" : LABEL_ABS, // TODO: differentiate with let + "}{\\textrm A{\\small BS}}}" : LABEL_ABS,
UIC)); UIC));
absL.getPremise().accept(this); absL.getPremise().accept(this);
} }
@ -174,9 +174,8 @@ public class LatexCreator implements StepVisitor {
public void visit(VarStepWithLet varL) { public void visit(VarStepWithLet varL) {
String latex = ""; String latex = "";
if (mode == LatexCreatorMode.MATHJAX) { 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}}}"; + "typicalc-step-" + varL.getStepIndex() + "}{\\textrm V{\\small AR}}}";
// TODO: differentiate with let
} else { } else {
latex = LABEL_VAR; latex = LABEL_VAR;
} }