mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-09 10:50:42 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
251d5bd5c8
@ -56,7 +56,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
|
||||
* Needed for typeVisitor methods
|
||||
*/
|
||||
private String visitorBuffer = "";
|
||||
private boolean needsParentheses;
|
||||
private boolean needsParentheses = false;
|
||||
|
||||
/**
|
||||
* 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.stepLabels = stepLabels;
|
||||
|
||||
typeInferer.getFirstInferenceStep().accept(this);
|
||||
// typeInferer.getFirstInferenceStep().accept(this);
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the LaTeX-code for the proof tree
|
||||
*/
|
||||
protected String getTree() {
|
||||
return null;
|
||||
return "the $\\LaTeX$ inference tree should be here ";
|
||||
} // todo implement
|
||||
|
||||
/**
|
||||
* @return the LaTeX-code for constraints nad unification
|
||||
*/
|
||||
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
|
||||
|
||||
/**
|
||||
* @return the packages needed for the LaTeX-code from getTree() and getUnification()to work
|
||||
*/
|
||||
protected String getLatexPackages() {
|
||||
return null;
|
||||
return "the packages should be here";
|
||||
} // todo implement
|
||||
|
||||
private String conclusionToLatex(Conclusion conclusion) {
|
||||
|
@ -1,9 +1,10 @@
|
||||
package edu.kit.typicalc.view.content.typeinferencecontent;
|
||||
|
||||
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
|
||||
import com.vaadin.flow.component.ComponentUtil;
|
||||
import com.vaadin.flow.component.UI;
|
||||
import com.vaadin.flow.component.html.Div;
|
||||
import com.vaadin.flow.component.orderedlayout.Scroller;
|
||||
import com.vaadin.flow.router.BeforeEvent;
|
||||
import com.vaadin.flow.router.HasUrlParameter;
|
||||
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
||||
import com.vaadin.flow.router.PageTitle;
|
||||
import com.vaadin.flow.router.Route;
|
||||
import edu.kit.typicalc.model.TypeInfererInterface;
|
||||
@ -13,31 +14,37 @@ import edu.kit.typicalc.view.main.MainViewImpl;
|
||||
|
||||
@Route(value = "visualize", layout = MainViewImpl.class)
|
||||
@PageTitle("TypeInferenceView")
|
||||
public class TypeInferenceView extends HorizontalLayout
|
||||
implements ControlPanelView, HasUrlParameter<TypeInfererInterface> {
|
||||
public class TypeInferenceView extends VerticalLayout
|
||||
implements ControlPanelView {
|
||||
|
||||
private int currentStep;
|
||||
private int currentStep = 0;
|
||||
|
||||
private MathjaxUnification unification;
|
||||
private MathjaxProofTree tree;
|
||||
private TypeInfererInterface typeInferer;
|
||||
private Div content;
|
||||
private ControlPanel controlPanel;
|
||||
|
||||
public TypeInferenceView() {
|
||||
typeInferer = ComponentUtil.getData(UI.getCurrent(), TypeInfererInterface.class);
|
||||
setId("type-inference-view");
|
||||
add(new ControlPanel(this));
|
||||
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();
|
||||
}
|
||||
|
||||
@Override
|
||||
public void setParameter(BeforeEvent event, TypeInfererInterface typeInferer) {
|
||||
buildView(typeInferer);
|
||||
}
|
||||
|
||||
private void buildView(TypeInfererInterface typeInferer) {
|
||||
private void setContent() {
|
||||
// todo implement correctly
|
||||
LatexCreator lc = new LatexCreator(typeInferer);
|
||||
unification = new MathjaxUnification(lc.getUnification());
|
||||
tree = new MathjaxProofTree(lc.getTree());
|
||||
add(unification);
|
||||
add(new Scroller(tree));
|
||||
content.add(unification, tree);
|
||||
}
|
||||
|
||||
@Override
|
||||
@ -52,7 +59,7 @@ public class TypeInferenceView extends HorizontalLayout
|
||||
|
||||
@Override
|
||||
public void firstStepButton() {
|
||||
currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() - 1 : 0;
|
||||
currentStep = currentStep > tree.getStepCount() && tree.getStepCount() > 0 ? tree.getStepCount() - 1 : 0;
|
||||
refreshElements(currentStep);
|
||||
}
|
||||
|
||||
|
@ -6,6 +6,9 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
||||
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||
|
||||
/**
|
||||
* Container for the components displayed in the drawer area of the web page.
|
||||
*/
|
||||
@CssImport("./styles/view/main/drawer-content.css")
|
||||
public class DrawerContent extends VerticalLayout implements LocaleChangeObserver {
|
||||
|
||||
@ -20,7 +23,10 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
|
||||
private final H3 heading;
|
||||
private final VerticalLayout ruleContainer;
|
||||
|
||||
public DrawerContent() {
|
||||
/**
|
||||
* Creates a new DrawerContent.
|
||||
*/
|
||||
protected DrawerContent() {
|
||||
heading = new H3(getTranslation("root.inferenceRules"));
|
||||
ruleContainer = new VerticalLayout();
|
||||
ruleContainer.setId(RULE_CONTAINER_ID);
|
||||
|
@ -10,6 +10,11 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||
import java.util.List;
|
||||
import java.util.function.Consumer;
|
||||
|
||||
/**
|
||||
* Contains all predefined examples as buttons. Clicking on a button inserts the example string into
|
||||
* the input bar.
|
||||
*
|
||||
*/
|
||||
public class ExampleDialog extends Dialog implements LocaleChangeObserver {
|
||||
|
||||
private static final long serialVersionUID = 8718432784530464215L;
|
||||
@ -18,13 +23,22 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
|
||||
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)");
|
||||
private final Paragraph instruction;
|
||||
|
||||
public ExampleDialog(Consumer<String> callback) {
|
||||
/**
|
||||
* Creates a new ExampleDialog with a callback method to insert the example string into the input
|
||||
* bar.
|
||||
*
|
||||
* @param callback inserts the string of the chosen example into the input bar
|
||||
*/
|
||||
protected ExampleDialog(Consumer<String> callback) {
|
||||
VerticalLayout layout = new VerticalLayout();
|
||||
instruction = new Paragraph(getTranslation("root.selectExample"));
|
||||
layout.add(instruction);
|
||||
for (String term : EXAMPLES) {
|
||||
Button button = new Button(term);
|
||||
button.addClickListener(click -> callback.accept(term));
|
||||
button.addClickListener(click -> {
|
||||
callback.accept(term);
|
||||
this.close();
|
||||
});
|
||||
layout.add(button);
|
||||
}
|
||||
add(layout);
|
||||
|
@ -9,6 +9,9 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
||||
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||
|
||||
/**
|
||||
* Contains information on how to use the application.
|
||||
*/
|
||||
@CssImport("./styles/view/main/help-dialog.css")
|
||||
public class HelpDialog extends Dialog implements LocaleChangeObserver {
|
||||
private static final long serialVersionUID = 4470277770276296164L;
|
||||
@ -22,7 +25,10 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
|
||||
private final H3 heading;
|
||||
private final H5 inputSyntax;
|
||||
|
||||
public HelpDialog() {
|
||||
/**
|
||||
* Create a new HelpDialog.
|
||||
*/
|
||||
protected HelpDialog() {
|
||||
final HorizontalLayout headingLayout = new HorizontalLayout();
|
||||
heading = new H3(getTranslation("root.operatingHelp"));
|
||||
headingLayout.setId(HEADING_LAYOUT_ID);
|
||||
|
@ -12,6 +12,11 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
||||
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||
|
||||
/**
|
||||
* Visual representation of an inference rule. The component is composed of the rule itself (displayed
|
||||
* in LaTeX rendered by MathJax), the name of the rule and a button to copy the LaTeX-code to the
|
||||
* clipboard. Each InferenceRuleField is displayed in drawer area of the web page.
|
||||
*/
|
||||
@CssImport("./styles/view/main/inference-rule-field.css")
|
||||
@JsModule("./src/copy-to-clipboard.js")
|
||||
public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver {
|
||||
@ -31,7 +36,14 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
|
||||
private final H4 ruleName;
|
||||
private final MathjaxDisplay rule;
|
||||
|
||||
public InferenceRuleField(final String latex, final String nameKey) {
|
||||
/**
|
||||
* Initializes an InferenceRuleField with a key to get the name of the inference rule and the LaTeX-code
|
||||
* for its visual representation.
|
||||
*
|
||||
* @param latex the LaTeX-code
|
||||
* @param nameKey the key to get the name of the inference rule
|
||||
*/
|
||||
protected InferenceRuleField(final String latex, final String nameKey) {
|
||||
this.nameKey = nameKey;
|
||||
|
||||
final HorizontalLayout header = new HorizontalLayout();
|
||||
|
@ -1,5 +1,7 @@
|
||||
package edu.kit.typicalc.view.main;
|
||||
|
||||
import com.vaadin.flow.component.ComponentUtil;
|
||||
import com.vaadin.flow.component.UI;
|
||||
import com.vaadin.flow.component.applayout.AppLayout;
|
||||
import com.vaadin.flow.component.button.Button;
|
||||
import com.vaadin.flow.component.dependency.CssImport;
|
||||
@ -11,7 +13,6 @@ import com.vaadin.flow.component.notification.Notification.Position;
|
||||
import com.vaadin.flow.component.notification.NotificationVariant;
|
||||
import com.vaadin.flow.component.orderedlayout.FlexComponent;
|
||||
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
||||
|
||||
import edu.kit.typicalc.model.ModelImpl;
|
||||
import edu.kit.typicalc.model.TypeInfererInterface;
|
||||
import edu.kit.typicalc.model.parser.ParseError;
|
||||
@ -42,7 +43,8 @@ public class MainViewImpl extends AppLayout implements MainView {
|
||||
|
||||
@Override
|
||||
public void setTypeInferenceView(final TypeInfererInterface typeInferer) {
|
||||
this.getUI().ifPresent(ui -> ui.navigate(TypeInferenceView.class, typeInferer));
|
||||
ComponentUtil.setData(UI.getCurrent(), TypeInfererInterface.class, typeInferer);
|
||||
this.getUI().ifPresent(ui -> ui.navigate(TypeInferenceView.class));
|
||||
}
|
||||
|
||||
@Override
|
||||
|
Loading…
Reference in New Issue
Block a user