arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-09 10:50:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

enable mjx proof tree step functionality

Browse Source
This commit is contained in:
ucrhh 2021-01-29 00:19:21 +01:00
parent 20fc3fd892
commit c392cc0c0f
3 changed files with 51 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
frontend/src/mathjax-proof-tree.ts
View File

@ -2,16 +2,47 @@ import {MathjaxAdapter} from "./mathjax-adapter";
import {TemplateResult} from "lit-html";
class MathjaxProofTree extends MathjaxAdapter {
private steps: any[] = [];
render(): TemplateResult {
return super.render();
}
protected showStep(_n: number): void {
protected showStep(n: number): void {
for (let current = 0; current < this.steps.length; current++) {
if (current <= n) {
this.steps[current].style.display = "";
} else {
this.steps[current].style.display = "none";
}
}
}
protected calculateSteps(): void {
if (this.shadowRoot !== null) {
let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
let steps = [];
let a = null;
while (a = nodeIterator.nextNode()) {
// todo remove @ts suppress
// @ts-ignore
let semantics = a.getAttribute("semantics");
if (semantics == null || a.nodeName !== "g") {
continue;
}
if (semantics.startsWith("bspr_inference:") || semantics.startsWith("bspr_axiom")) {
steps.push(a);
// @ts-ignore
a.style.display = "none";
}
}
// @ts-ignore
this.steps = steps;
this.showStep(0);
// @ts-ignore
this.$server.setStepCount(steps.length);
}
}
}

12
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java
View File

@ -1,5 +1,6 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.ClientCallable;
import com.vaadin.flow.component.Tag;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
@ -16,6 +17,8 @@ import edu.kit.typicalc.view.MathjaxAdapter;
@JsModule("./src/mathjax-proof-tree.ts")
public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
private int stepCount = -1;
@Id("tc-content")
private Div content;
@ -29,14 +32,19 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
content.add(latex);
}
@ClientCallable
private void setStepCount(int stepCount) {
this.stepCount = stepCount;
}
@Override
public int getStepCount() {
return 0;
return this.stepCount;
}
@Override
public void showStep(int n) {
getElement().callJsFunction("showStep", n);
}
@Override

11
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java
View File

@ -1,5 +1,6 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.ClientCallable;
import com.vaadin.flow.component.Tag;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
@ -15,6 +16,8 @@ import edu.kit.typicalc.view.MathjaxAdapter;
@JsModule("./src/mathjax-unification.ts")
public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
private int stepCount = -1;
@Id("tc-content")
private Div content;
@ -27,10 +30,14 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
content.add(latex);
}
@ClientCallable
private void setStepCount(int stepCount) {
this.stepCount = stepCount;
}
@Override
public int getStepCount() {
// todo implement
return 0;
return this.stepCount;
}
@Override