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

Fix checkstyle issue

Browse Source
This commit is contained in:
Arne Keller 2021-02-10 08:24:31 +01:00
parent 54da12a132
commit 3e153dc0d3
2 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -4,9 +4,9 @@ SVGElement.prototype.getTransformToElement = SVGElement.prototype.getTransformTo
return elem.getScreenCTM().inverse().multiply(this.getScreenCTM());
};
window.MathJax = {
loader: {load: ['input/tex-full', 'output/svg', '[tex]/bussproofs', '[tex]/unicode']},
loader: {load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/textmacros', '[tex]/unicode']},
tex: {
packages: {'[+]': ['bussproofs', 'unicode']},
packages: {'[+]': ['ams', 'bussproofs', 'textmacros', 'unicode']},
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
svg: {

3
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java
View File

@ -56,7 +56,8 @@ public class LatexCreatorConstraints implements StepVisitor {
typeInferer.getMGU().ifPresent(mgu -> {
result.add(generateMGU());
numberGenerator.push();
result.add(generateMGU() + LATEX_NEW_LINE + new LatexCreatorType(typeInferer.getType().get()).getLatex());
result.add(generateMGU() + LATEX_NEW_LINE
+ new LatexCreatorType(typeInferer.getType().get()).getLatex());
numberGenerator.push();
});
// todo add some helpful text for the user