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

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
Moritz Dieing 2021-01-30 14:52:02 +01:00
commit 456c235009
2 changed files with 26 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -56,7 +56,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
* Needed for typeVisitor methods * Needed for typeVisitor methods
*/ */
private String visitorBuffer = ""; private String visitorBuffer = "";
private boolean needsParentheses; private boolean needsParentheses = false;
/** /**
* Generate the pieces of LaTeX-code from the type inferer. * Generate the pieces of LaTeX-code from the type inferer.
@ -71,28 +71,30 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
this.tree = new StringBuilder(); this.tree = new StringBuilder();
this.stepLabels = stepLabels; this.stepLabels = stepLabels;
typeInferer.getFirstInferenceStep().accept(this); // typeInferer.getFirstInferenceStep().accept(this);
} }
/** /**
* @return the LaTeX-code for the proof tree * @return the LaTeX-code for the proof tree
*/ */
protected String getTree() { protected String getTree() {
return null; return "the $\\LaTeX$ inference tree should be here ";
} // todo implement } // todo implement
/** /**
* @return the LaTeX-code for constraints nad unification * @return the LaTeX-code for constraints nad unification
*/ */
protected String[] getUnification() { protected String[] getUnification() {
return null; return new String[]{"$\\tau_0$", "$\\tau_1$", "$\\tau_2$", "$\\tau_3$", "$\\tau_4$",
"$\\tau_5$", "$\\tau_6$", "$\\tau_7$", "$\\tau_8$", "$\\tau_9$", "$\\tau_{10}$", "$\\tau_{11}$",
"$\\tau_{12}$", "$\\tau_{13}$", "$\\tau_{14}$"};
} // todo implement } // todo implement
/** /**
* @return the packages needed for the LaTeX-code from getTree() and getUnification()to work * @return the packages needed for the LaTeX-code from getTree() and getUnification()to work
*/ */
protected String getLatexPackages() { protected String getLatexPackages() {
return null; return "the packages should be here";
} // todo implement } // todo implement
private String conclusionToLatex(Conclusion conclusion) { private String conclusionToLatex(Conclusion conclusion) {

28
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java
View File

@ -2,8 +2,9 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.ComponentUtil; import com.vaadin.flow.component.ComponentUtil;
import com.vaadin.flow.component.UI; import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.orderedlayout.Scroller; import com.vaadin.flow.component.orderedlayout.Scroller;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.router.PageTitle; import com.vaadin.flow.router.PageTitle;
import com.vaadin.flow.router.Route; import com.vaadin.flow.router.Route;
import edu.kit.typicalc.model.TypeInfererInterface; import edu.kit.typicalc.model.TypeInfererInterface;
@ -13,28 +14,37 @@ import edu.kit.typicalc.view.main.MainViewImpl;
@Route(value = "visualize", layout = MainViewImpl.class) @Route(value = "visualize", layout = MainViewImpl.class)
@PageTitle("TypeInferenceView") @PageTitle("TypeInferenceView")
public class TypeInferenceView extends HorizontalLayout public class TypeInferenceView extends VerticalLayout
implements ControlPanelView { implements ControlPanelView {
private int currentStep; private int currentStep = 0;
private MathjaxUnification unification; private MathjaxUnification unification;
private MathjaxProofTree tree; private MathjaxProofTree tree;
private TypeInfererInterface typeInferer; private TypeInfererInterface typeInferer;
private Div content;
private ControlPanel controlPanel;
public TypeInferenceView() { public TypeInferenceView() {
setId("type-inference-view");
add(new ControlPanel(this));
typeInferer = ComponentUtil.getData(UI.getCurrent(), TypeInfererInterface.class); typeInferer = ComponentUtil.getData(UI.getCurrent(), TypeInfererInterface.class);
setId("type-inference-view");
setSizeFull();
content = new Div();
controlPanel = new ControlPanel(this);
Scroller scroller = new Scroller(content);
scroller.setSizeFull();
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
setAlignItems(Alignment.CENTER);
add(scroller, controlPanel);
setContent();
} }
private void buildView() { private void setContent() {
// todo implement correctly // todo implement correctly
LatexCreator lc = new LatexCreator(typeInferer); LatexCreator lc = new LatexCreator(typeInferer);
unification = new MathjaxUnification(lc.getUnification()); unification = new MathjaxUnification(lc.getUnification());
tree = new MathjaxProofTree(lc.getTree()); tree = new MathjaxProofTree(lc.getTree());
add(unification); content.add(unification, tree);
add(new Scroller(tree));
} }
@Override @Override
@ -49,7 +59,7 @@ public class TypeInferenceView extends HorizontalLayout
@Override @Override
public void firstStepButton() { public void firstStepButton() {
currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() - 1 : 0; currentStep = currentStep > tree.getStepCount() && tree.getStepCount() > 0 ? tree.getStepCount() - 1 : 0;
refreshElements(currentStep); refreshElements(currentStep);
} }