Commit 2bc908e6 authored by Arne Keller's avatar Arne Keller
Browse files

Fix explanation text language switch

closes #30
parent cbe7d47c
Pipeline #168818 passed with stages
in 9 minutes and 55 seconds
......@@ -15,17 +15,17 @@ class MathjaxExplanation extends MathjaxAdapter {
}
protected calculateSteps(_extraData: any) {
let first = true;
let stepIdx = 0;
for (let text of this.shadowRoot!.querySelectorAll<SVGGraphicsElement>(".tc-text")) {
for (let text of this.shadowRoot!.querySelectorAll<HTMLElement>(".tc-text")) {
let thisStepIdx = stepIdx;
stepIdx++;
text.onclick = () => {
// @ts-ignore
this.$server!.switchToStep(thisStepIdx);
};
if (first) {
first = false; // show first step
// show initial step
if (thisStepIdx === this.lastStepShown) {
this.scrollToElementIfNeeded(text);
continue;
}
text.style.opacity = "0.5";
......@@ -38,19 +38,22 @@ class MathjaxExplanation extends MathjaxAdapter {
lastEl.style.opacity = "0.5";
}
let el = this.getElementForStep(n);
this.lastStepShown = n;
if (el) {
this.lastStepShown = n;
// scroll to element if needed
const hostEl = this.shadowRoot!.host as HTMLElement;
const dy = el.offsetTop - hostEl.offsetTop - hostEl.scrollTop;
// end of text is below the container or the start of the text is above the container:
if (dy + el.offsetHeight > hostEl.offsetHeight || dy < 0) {
hostEl.scrollBy(0, -hostEl.scrollTop + el.offsetTop - hostEl.offsetTop);
}
this.scrollToElementIfNeeded(el);
el.style.opacity = "1.0";
}
}
private scrollToElementIfNeeded(el: HTMLElement) {
const hostEl = this.shadowRoot!.host as HTMLElement;
const dy = el.offsetTop - hostEl.offsetTop - hostEl.scrollTop;
// end of text is below the container or the start of the text is above the container:
if (dy + el.offsetHeight > hostEl.offsetHeight || dy < 0) {
hostEl.scrollBy(0, -hostEl.scrollTop + el.offsetTop - hostEl.offsetTop);
}
}
private getElementForStep(n: number): HTMLElement | null {
return this.shadowRoot!.getElementById("tc-text-" + n)
}
......
......@@ -34,8 +34,9 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
*
* @param view the type inference view this explanation text is attached to
* @param latex the latex texts for all steps
* @param initialStep the step to show initially
*/
public MathjaxExplanation(TypeInferenceView view, List<String> latex) {
public MathjaxExplanation(TypeInferenceView view, List<String> latex, int initialStep) {
this.typeInferenceView = view;
this.latex = latex;
StringBuilder finalTex = new StringBuilder("<div>");
......@@ -46,7 +47,7 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
}
var finalString = finalTex.append("</div>").toString();
content.add(new Html(finalString));
showStep(0);
showStep(initialStep);
}
@Override
......
......@@ -130,7 +130,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(this, explainer.getExplanationTexts());
this.explanation = new MathjaxExplanation(this, explainer.getExplanationTexts(), this.currentStep);
if (tree == null) {
tree = new MathjaxProofTree(lc.getTree(), stepAnnotations);
......@@ -144,7 +144,6 @@ public class TypeInferenceView extends VerticalLayout
TypeInferenceRules rules = new TypeInferenceRules();
rules.setId(RULES_ID);
rulesVisible = false;
rules.getElement().setVisible(rulesVisible);
button.addClickListener(e -> {
rulesVisible = !rulesVisible;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment