diff --git a/frontend/src/mathjax-explanation.ts b/frontend/src/mathjax-explanation.ts index ad49384..c6ba004 100644 --- a/frontend/src/mathjax-explanation.ts +++ b/frontend/src/mathjax-explanation.ts @@ -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(".tc-text")) { + let thisStepIdx = stepIdx; + stepIdx++; + text.onclick = () => { + // @ts-ignore + this.$server!.switchToStep(thisStepIdx); + }; if (first) { first = false; // show first step continue; diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java index 9649b09..9c2de43 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxExplanation.java @@ -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 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 latex) { + public MathjaxExplanation(TypeInferenceView view, List latex) { + this.typeInferenceView = view; this.latex = latex; StringBuilder finalTex = new StringBuilder("
"); for (int i = 0; i < latex.size(); i++) { - finalTex.append("

"); + finalTex.append(String.format("

", i)); finalTex.append(latex.get(i)); finalTex.append("

"); } @@ -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); + } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index 7ccee51..e526289 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java @@ -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) {