mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-13 20:53:09 +00:00
add skeletons for all Mathjax classes
This commit is contained in:
parent
e4dfba29ef
commit
20fc3fd892
18
frontend/src/mathjax-unification.ts
Normal file
18
frontend/src/mathjax-unification.ts
Normal file
@ -0,0 +1,18 @@
|
|||||||
|
import {MathjaxAdapter} from "./mathjax-adapter";
|
||||||
|
import {TemplateResult} from "lit-html";
|
||||||
|
|
||||||
|
class MathjaxUnification extends MathjaxAdapter {
|
||||||
|
|
||||||
|
render(): TemplateResult {
|
||||||
|
return super.render();
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
protected showStep(_n: number): void {
|
||||||
|
}
|
||||||
|
|
||||||
|
protected calculateSteps(): void {
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
customElements.define('tc-unification', MathjaxUnification);
|
@ -1,20 +1,15 @@
|
|||||||
package edu.kit.typicalc.view;
|
package edu.kit.typicalc.view;
|
||||||
|
|
||||||
import com.vaadin.flow.component.littemplate.LitTemplate;
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Represents an HTML element that uses MathJax and custom JavaScript classes to render its contents.
|
* Represents an HTML element that uses MathJax and custom JavaScript classes to render its contents.
|
||||||
* Provides an interface between Java code and said JavaScript classes. Allows to reveal parts of the
|
* Provides an interface between Java code and said JavaScript classes. Allows to reveal parts of the
|
||||||
* rendered LaTeX step-by-step. Allows for scaling of the rendered LaTeX.
|
* rendered LaTeX step-by-step. Allows for scaling of the rendered LaTeX.
|
||||||
*/
|
*/
|
||||||
public abstract class MathjaxAdapter extends LitTemplate {
|
public interface MathjaxAdapter {
|
||||||
|
|
||||||
/**
|
int getStepCount();
|
||||||
* Creates a new HTML element that renders the LaTeX string passed as parameter using MathJax. Because
|
|
||||||
* MathJax is used to render the String, all LaTeX commands used must be MathJax compatible.
|
|
||||||
* @param latex the LaTex string to render with MathJax
|
|
||||||
*/
|
|
||||||
protected MathjaxAdapter(String latex) {
|
|
||||||
|
|
||||||
}
|
void showStep(int n);
|
||||||
|
|
||||||
|
void scale(double newScaling);
|
||||||
}
|
}
|
||||||
|
@ -7,6 +7,7 @@ import com.vaadin.flow.router.PageTitle;
|
|||||||
import com.vaadin.flow.router.Route;
|
import com.vaadin.flow.router.Route;
|
||||||
import com.vaadin.flow.router.RouteAlias;
|
import com.vaadin.flow.router.RouteAlias;
|
||||||
import edu.kit.typicalc.view.content.typeinferencecontent.MathjaxProofTree;
|
import edu.kit.typicalc.view.content.typeinferencecontent.MathjaxProofTree;
|
||||||
|
import edu.kit.typicalc.view.content.typeinferencecontent.MathjaxUnification;
|
||||||
import edu.kit.typicalc.view.main.MainViewImpl;
|
import edu.kit.typicalc.view.main.MainViewImpl;
|
||||||
import edu.kit.typicalc.view.main.MathjaxDisplay;
|
import edu.kit.typicalc.view.main.MathjaxDisplay;
|
||||||
|
|
||||||
@ -21,8 +22,9 @@ public class StartPageView extends VerticalLayout {
|
|||||||
public StartPageView() {
|
public StartPageView() {
|
||||||
// todo implement correctly
|
// todo implement correctly
|
||||||
setId("start-page");
|
setId("start-page");
|
||||||
add(new MathjaxDisplay());
|
add(new MathjaxDisplay(getTranslation("abs-rule")));
|
||||||
add(new MathjaxProofTree());
|
add(new MathjaxUnification("\\(constraint test \\vdash \\)"));
|
||||||
|
add(new MathjaxProofTree(getTranslation("demo-tree")));
|
||||||
sayHello = new Button("Say hello");
|
sayHello = new Button("Say hello");
|
||||||
add(sayHello);
|
add(sayHello);
|
||||||
}
|
}
|
||||||
|
@ -5,18 +5,43 @@ import com.vaadin.flow.component.dependency.JsModule;
|
|||||||
import com.vaadin.flow.component.html.Div;
|
import com.vaadin.flow.component.html.Div;
|
||||||
import com.vaadin.flow.component.littemplate.LitTemplate;
|
import com.vaadin.flow.component.littemplate.LitTemplate;
|
||||||
import com.vaadin.flow.component.template.Id;
|
import com.vaadin.flow.component.template.Id;
|
||||||
|
import edu.kit.typicalc.view.MathjaxAdapter;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Renders a tree from LaTeX using MathJax and allows for step-by-step-revealing for
|
||||||
|
* proof trees that use the bussproofs package. Relies on MathjaxProofTreeJS to interact
|
||||||
|
* with MathJax.
|
||||||
|
*/
|
||||||
@Tag("tc-proof-tree")
|
@Tag("tc-proof-tree")
|
||||||
@JsModule("./src/mathjax-proof-tree.ts")
|
@JsModule("./src/mathjax-proof-tree.ts")
|
||||||
public class MathjaxProofTree extends LitTemplate {
|
public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
|
||||||
|
|
||||||
@Id("tc-content")
|
@Id("tc-content")
|
||||||
private Div content;
|
private Div content;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* todo Creates the hello world template.
|
* Creates a new HTML element that renders the proof tree and cuts it into steps.
|
||||||
|
* The latex String must consist of exactly one proof tree environment in order for
|
||||||
|
* this element to work. In other cases the expected behaviour is undefined.
|
||||||
|
* @param latex the LaTeX-String to render with MathJax
|
||||||
*/
|
*/
|
||||||
public MathjaxProofTree() {
|
public MathjaxProofTree(String latex) {
|
||||||
content.add(getTranslation("demo-tree"));
|
content.add(latex);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int getStepCount() {
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void showStep(int n) {
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void scale(double newScaling) {
|
||||||
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -0,0 +1,46 @@
|
|||||||
|
package edu.kit.typicalc.view.content.typeinferencecontent;
|
||||||
|
|
||||||
|
import com.vaadin.flow.component.Tag;
|
||||||
|
import com.vaadin.flow.component.dependency.JsModule;
|
||||||
|
import com.vaadin.flow.component.html.Div;
|
||||||
|
import com.vaadin.flow.component.littemplate.LitTemplate;
|
||||||
|
import com.vaadin.flow.component.template.Id;
|
||||||
|
import edu.kit.typicalc.view.MathjaxAdapter;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Renders the constraints and unification from LaTeX using MathJax and allows step-by-
|
||||||
|
* step-revealing capabilities. Relies on MathjaxUnificationJS to interact with MathJax.
|
||||||
|
*/
|
||||||
|
@Tag("tc-unification")
|
||||||
|
@JsModule("./src/mathjax-unification.ts")
|
||||||
|
public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
|
||||||
|
|
||||||
|
@Id("tc-content")
|
||||||
|
private Div content;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Creates a new HTML element that renders the constraints and unification and
|
||||||
|
* calculates the steps.
|
||||||
|
* @param latex the LaTeX-String to render with MathJax
|
||||||
|
*/
|
||||||
|
public MathjaxUnification(String latex) {
|
||||||
|
content.add(latex);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int getStepCount() {
|
||||||
|
// todo implement
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void showStep(int n) {
|
||||||
|
// todo implement
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void scale(double newScaling) {
|
||||||
|
// todo implement
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -5,18 +5,40 @@ import com.vaadin.flow.component.dependency.JsModule;
|
|||||||
import com.vaadin.flow.component.html.Div;
|
import com.vaadin.flow.component.html.Div;
|
||||||
import com.vaadin.flow.component.littemplate.LitTemplate;
|
import com.vaadin.flow.component.littemplate.LitTemplate;
|
||||||
import com.vaadin.flow.component.template.Id;
|
import com.vaadin.flow.component.template.Id;
|
||||||
|
import edu.kit.typicalc.view.MathjaxAdapter;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Renders static LaTeX content using MathJax. Relies on MathjaxDisplayJS to interact
|
||||||
|
* with MathJax.
|
||||||
|
*/
|
||||||
@Tag("tc-display")
|
@Tag("tc-display")
|
||||||
@JsModule("./src/mathjax-display.ts")
|
@JsModule("./src/mathjax-display.ts")
|
||||||
public class MathjaxDisplay extends LitTemplate {
|
public class MathjaxDisplay extends LitTemplate implements MathjaxAdapter {
|
||||||
|
|
||||||
@Id("tc-content")
|
@Id("tc-content")
|
||||||
private Div content;
|
private Div content;
|
||||||
/**
|
/**
|
||||||
* todo Creates the hello world template.
|
* Creates a new HTML element that renders the LaTeX code.
|
||||||
|
*
|
||||||
|
* @param latex the LaTeX string to render with MathJax
|
||||||
*/
|
*/
|
||||||
public MathjaxDisplay() {
|
public MathjaxDisplay(String latex) {
|
||||||
content.add(getTranslation("abs-rule"));
|
content.add(latex);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int getStepCount() {
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void showStep(int n) {
|
||||||
|
// do nothing
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void scale(double newScaling) {
|
||||||
|
// todo implement
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user