mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
add amsmath to needed packages
This commit is contained in:
parent
a442f5caf5
commit
c2de56a29a
@ -25,7 +25,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
private static final String CLOSE_ICON_ID = "closeIcon";
|
private static final String CLOSE_ICON_ID = "closeIcon";
|
||||||
|
|
||||||
private final TextField urlField;
|
private final TextField urlField;
|
||||||
private final TextField packageField;
|
private final TextArea packageArea;
|
||||||
private final TextArea latexArea;
|
private final TextArea latexArea;
|
||||||
private final H3 heading;
|
private final H3 heading;
|
||||||
|
|
||||||
@ -34,11 +34,9 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
* to the String that is passed as corresponding parameter.
|
* to the String that is passed as corresponding parameter.
|
||||||
*
|
*
|
||||||
* @param url a permalink to share with other users
|
* @param url a permalink to share with other users
|
||||||
* @param latexPackages the needed LaTeX-packages to use the displayed mathematics
|
|
||||||
* in other LaTeX documents. Should be in the form „\\usepackage<package>“
|
|
||||||
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
|
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
|
||||||
*/
|
*/
|
||||||
public ShareDialog(String url, String latexPackages, String latexCode) {
|
public ShareDialog(String url, String latexCode) {
|
||||||
HorizontalLayout headingLayout = new HorizontalLayout();
|
HorizontalLayout headingLayout = new HorizontalLayout();
|
||||||
headingLayout.setId(HEADING_LAYOUT_ID);
|
headingLayout.setId(HEADING_LAYOUT_ID);
|
||||||
|
|
||||||
@ -55,17 +53,17 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
setId(SHARE_DIALOG_ID);
|
setId(SHARE_DIALOG_ID);
|
||||||
|
|
||||||
urlField = new TextField();
|
urlField = new TextField();
|
||||||
packageField = new TextField();
|
packageArea = new TextArea();
|
||||||
latexArea = new TextArea();
|
latexArea = new TextArea();
|
||||||
|
|
||||||
urlField.setValue(url);
|
urlField.setValue(url);
|
||||||
urlField.setClassName(FIELD_CLASS);
|
urlField.setClassName(FIELD_CLASS);
|
||||||
packageField.setValue(latexPackages);
|
packageArea.setValue(getTranslation("share.neededPackages"));
|
||||||
packageField.setClassName(FIELD_CLASS);
|
packageArea.setClassName(FIELD_CLASS);
|
||||||
latexArea.setValue(latexCode);
|
latexArea.setValue(latexCode);
|
||||||
latexArea.setClassName(FIELD_CLASS);
|
latexArea.setClassName(FIELD_CLASS);
|
||||||
|
|
||||||
layout.add(urlField, packageField, latexArea);
|
layout.add(urlField, packageArea, latexArea);
|
||||||
|
|
||||||
add(headingLayout, layout);
|
add(headingLayout, layout);
|
||||||
}
|
}
|
||||||
@ -75,7 +73,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
public void localeChange(LocaleChangeEvent localeChangeEvent) {
|
public void localeChange(LocaleChangeEvent localeChangeEvent) {
|
||||||
heading.setText(getTranslation("share.heading"));
|
heading.setText(getTranslation("share.heading"));
|
||||||
urlField.setLabel(getTranslation("share.url.label"));
|
urlField.setLabel(getTranslation("share.url.label"));
|
||||||
packageField.setLabel(getTranslation("share.packages.label"));
|
packageArea.setLabel(getTranslation("share.packages.label"));
|
||||||
latexArea.setLabel(getTranslation("share.latex.label"));
|
latexArea.setLabel(getTranslation("share.latex.label"));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -82,7 +82,7 @@ public class TypeInferenceView extends VerticalLayout
|
|||||||
@Override
|
@Override
|
||||||
public void shareButton() {
|
public void shareButton() {
|
||||||
UI.getCurrent().getPage().executeJs("return decodeURI(window.location.href)").then(url ->
|
UI.getCurrent().getPage().executeJs("return decodeURI(window.location.href)").then(url ->
|
||||||
new ShareDialog(url.asString(), lc.getLatexPackages(), lc.getTree()).open()
|
new ShareDialog(url.asString(), lc.getTree()).open()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -77,16 +77,6 @@ public class LatexCreator implements StepVisitor {
|
|||||||
return constraintsCreator.getTreeNumbers();
|
return constraintsCreator.getTreeNumbers();
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
|
||||||
* Returns needed LaTeX packages
|
|
||||||
*
|
|
||||||
* @return the packages needed for the LaTeX-code from getTree() to work
|
|
||||||
*/
|
|
||||||
public String getLatexPackages() {
|
|
||||||
return BUSSPROOFS;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
private String conclusionToLatex(Conclusion conclusion) {
|
private String conclusionToLatex(Conclusion conclusion) {
|
||||||
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());
|
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());
|
||||||
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
|
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
|
||||||
@ -155,8 +145,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
|
tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
|
||||||
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
|
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
|
||||||
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
|
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
|
||||||
String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType
|
String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType + DOLLAR_SIGN;
|
||||||
+ DOLLAR_SIGN + NEW_LINE;
|
|
||||||
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
|
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
|
||||||
+ generateVarStepPremise(varL).replace(DOLLAR_SIGN, "")
|
+ generateVarStepPremise(varL).replace(DOLLAR_SIGN, "")
|
||||||
+ SPACE + LATEX_NEW_LINE + SPACE // todo less replacement fixups
|
+ SPACE + LATEX_NEW_LINE + SPACE // todo less replacement fixups
|
||||||
|
@ -74,6 +74,4 @@ public final class LatexCreatorConstants {
|
|||||||
protected static final String ALIGN_END = "\\end{aligned}";
|
protected static final String ALIGN_END = "\\end{aligned}";
|
||||||
protected static final String SPLIT_BEGIN = "\\begin{split}";
|
protected static final String SPLIT_BEGIN = "\\begin{split}";
|
||||||
protected static final String SPLIT_END = "\\end{split}";
|
protected static final String SPLIT_END = "\\end{split}";
|
||||||
|
|
||||||
protected static final String BUSSPROOFS = "\\usepackage{bussproofs}";
|
|
||||||
}
|
}
|
||||||
|
@ -79,4 +79,8 @@ root.varLetLatex=\
|
|||||||
\
|
\
|
||||||
\\LeftLabel{\\textrm V{\\small AR}}\
|
\\LeftLabel{\\textrm V{\\small AR}}\
|
||||||
\\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\
|
\\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\
|
||||||
\\end{prooftree}
|
\\end{prooftree}
|
||||||
|
|
||||||
|
share.neededPackages=\
|
||||||
|
\\usepackage{bussproofs}\n\
|
||||||
|
\\usepackage{amsmath}
|
Loading…
Reference in New Issue
Block a user