mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-09 10:50:42 +00:00
Optimize unification view
This commit is contained in:
parent
520960fea1
commit
29d692c231
@ -13,9 +13,7 @@ class MathjaxUnification extends MathjaxAdapter {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
protected showStep(_n: number): void {
|
protected showStep(_n: number): void {}
|
||||||
this.requestTypeset(null);
|
|
||||||
}
|
|
||||||
|
|
||||||
protected calculateSteps(_extraData: any) {
|
protected calculateSteps(_extraData: any) {
|
||||||
const root = this.shadowRoot!;
|
const root = this.shadowRoot!;
|
||||||
@ -37,6 +35,16 @@ class MathjaxUnification extends MathjaxAdapter {
|
|||||||
prooftree.handleHoverEvent(e as MouseEvent, false);
|
prooftree.handleHoverEvent(e as MouseEvent, false);
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
protected showLatex(code: string): void {
|
||||||
|
let el = this.shadowRoot!.getElementById("tc-content");
|
||||||
|
if (!el) {
|
||||||
|
setTimeout(() => this.showLatex(code), 50);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
el.innerHTML = code;
|
||||||
|
this.requestTypeset(null);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
customElements.define('tc-unification', MathjaxUnification);
|
customElements.define('tc-unification', MathjaxUnification);
|
||||||
|
@ -41,7 +41,7 @@
|
|||||||
}
|
}
|
||||||
|
|
||||||
tc-explanation {
|
tc-explanation {
|
||||||
max-width: 40em;
|
width: 100em;
|
||||||
padding-left: 1em;
|
padding-left: 1em;
|
||||||
padding-right: 1em;
|
padding-right: 1em;
|
||||||
overflow-y: auto;
|
overflow-y: auto;
|
||||||
|
@ -43,12 +43,7 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
|
|||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void showStep(int n) {
|
public void showStep(int n) {
|
||||||
if (n < latex.length) {
|
getElement().callJsFunction("showLatex", latex[n]);
|
||||||
content.removeAll();
|
|
||||||
// add latex as HTML because <br> is used in the latex code
|
|
||||||
content.add(new Html("<div>" + latex[n] + "</div>"));
|
|
||||||
}
|
|
||||||
getElement().callJsFunction("showStep", n);
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user