mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-09-18 17:55:14 +00:00
parent
8b1371ce08
commit
5d4d8cd828
@ -16,7 +16,14 @@ class MathjaxExplanation extends MathjaxAdapter {
|
||||
|
||||
protected calculateSteps(_extraData: any) {
|
||||
let first = true;
|
||||
let stepIdx = 0;
|
||||
for (let text of this.shadowRoot!.querySelectorAll<SVGGraphicsElement>(".tc-text")) {
|
||||
let thisStepIdx = stepIdx;
|
||||
stepIdx++;
|
||||
text.onclick = () => {
|
||||
// @ts-ignore
|
||||
this.$server!.switchToStep(thisStepIdx);
|
||||
};
|
||||
if (first) {
|
||||
first = false; // show first step
|
||||
continue;
|
||||
|
@ -1,5 +1,6 @@
|
||||
package edu.kit.typicalc.view.content.typeinferencecontent;
|
||||
|
||||
import com.vaadin.flow.component.ClientCallable;
|
||||
import com.vaadin.flow.component.Html;
|
||||
import com.vaadin.flow.component.Tag;
|
||||
import com.vaadin.flow.component.dependency.CssImport;
|
||||
@ -21,6 +22,7 @@ import java.util.List;
|
||||
@CssImport("./styles/view/explanation.css")
|
||||
public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
|
||||
|
||||
private final TypeInferenceView typeInferenceView;
|
||||
private final List<String> latex;
|
||||
|
||||
// initialized by Vaadin
|
||||
@ -30,13 +32,15 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
|
||||
/**
|
||||
* Creates a new HTML element that renders the provided texts.
|
||||
*
|
||||
* @param view the type inference view this explanation text is attached to
|
||||
* @param latex the latex texts for all steps
|
||||
*/
|
||||
public MathjaxExplanation(List<String> latex) {
|
||||
public MathjaxExplanation(TypeInferenceView view, List<String> latex) {
|
||||
this.typeInferenceView = view;
|
||||
this.latex = latex;
|
||||
StringBuilder finalTex = new StringBuilder("<div>");
|
||||
for (int i = 0; i < latex.size(); i++) {
|
||||
finalTex.append("<p class='tc-text' id='tc-text-").append(i).append("'>");
|
||||
finalTex.append(String.format("<p class='tc-text' id='tc-text-%d'>", i));
|
||||
finalTex.append(latex.get(i));
|
||||
finalTex.append("</p>");
|
||||
}
|
||||
@ -54,5 +58,10 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
|
||||
public void showStep(int n) {
|
||||
getElement().callJsFunction("showStep", n);
|
||||
}
|
||||
|
||||
@ClientCallable
|
||||
private void switchToStep(int unificationStepIdx) {
|
||||
typeInferenceView.setCurrentStep(unificationStepIdx);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -123,7 +123,7 @@ public class TypeInferenceView extends VerticalLayout
|
||||
container.setId(CONTENT_ID2);
|
||||
unification = new MathjaxUnification(lc.getUnification());
|
||||
var explainer = new ExplanationCreator(typeInferer, getLocale());
|
||||
this.explanation = new MathjaxExplanation(explainer.getExplanationTexts());
|
||||
this.explanation = new MathjaxExplanation(this, explainer.getExplanationTexts());
|
||||
|
||||
if (tree == null) {
|
||||
tree = new MathjaxProofTree(lc.getTree(), stepAnnotations);
|
||||
@ -209,6 +209,11 @@ public class TypeInferenceView extends VerticalLayout
|
||||
refreshElements();
|
||||
}
|
||||
|
||||
public void setCurrentStep(int step) {
|
||||
currentStep = step;
|
||||
refreshElements();
|
||||
}
|
||||
|
||||
@Override
|
||||
public void localeChange(LocaleChangeEvent localeChangeEvent) {
|
||||
if (typeInferer != null) {
|
||||
|
Loading…
Reference in New Issue
Block a user