From 1d53bdfe7573ef337f9dc1ee0ed597a75a9c87b7 Mon Sep 17 00:00:00 2001 From: ucrhh Date: Thu, 11 Mar 2021 00:37:36 +0100 Subject: [PATCH] first implementation of unification export --- .../typeinferencecontent/ShareDialog.java | 48 +++++++++++++------ .../TypeInferenceView.java | 5 +- .../latexcreator/LatexCreatorConstants.java | 7 ++- .../resources/language/general.properties | 8 +++- .../language/translation_de.properties | 6 ++- .../language/translation_en.properties | 6 ++- 6 files changed, 57 insertions(+), 23 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java index b7808a4..3da466e 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java @@ -13,6 +13,9 @@ import com.vaadin.flow.component.textfield.TextArea; import com.vaadin.flow.component.textfield.TextField; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; +import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants; + +import java.util.regex.Pattern; /** * Contains GUI elements to extract the URL and LaTeX code of the currently shown proof tree. @@ -27,9 +30,13 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver { private static final String FIELD_CLASS = "share-dialog-field"; private static final String CLOSE_ICON_ID = "closeIcon"; + private static final String RIGHT_ARROW_WHITE = "\\\\rightwhitearrow"; + private final TextField urlField; - private final TextArea packageArea; - private final TextArea latexArea; + private final TextArea packageAreaTree; + private final TextArea packageAreaUnification; + private final TextArea latexAreaTree; + private final TextArea latexAreaUnification; private final H3 heading; /** @@ -37,9 +44,9 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver { * to the String that is passed as corresponding parameter. * * @param url a permalink to share with other users - * @param latexCode LaTeX code for users to copy into their own LaTeX document(s) + * @param latexCodeTree LaTeX code for the tree for users to copy into their own LaTeX document(s) */ - public ShareDialog(String url, String latexCode) { + public ShareDialog(String url, String latexCodeTree, String latexCodeUnification) { HorizontalLayout headingLayout = new HorizontalLayout(); headingLayout.setId(HEADING_LAYOUT_ID); @@ -56,20 +63,27 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver { setId(SHARE_DIALOG_ID); urlField = new TextField(); - packageArea = new TextArea(); - latexArea = new TextArea(); + packageAreaTree = new TextArea(); + latexAreaTree = new TextArea(); + packageAreaUnification = new TextArea(); + latexAreaUnification = new TextArea(); urlField.setValue(url); urlField.setClassName(FIELD_CLASS); - packageArea.setValue(getTranslation("share.neededPackages")); - packageArea.setClassName(FIELD_CLASS); - latexArea.setValue(latexCode); - latexArea.setClassName(FIELD_CLASS); + packageAreaTree.setValue(getTranslation("share.neededPackagesTree")); //todo + packageAreaTree.setClassName(FIELD_CLASS); + packageAreaUnification.setValue(getTranslation("share.neededPackagesUnification")); //todo + packageAreaUnification.setClassName(FIELD_CLASS); + latexAreaTree.setValue(latexCodeTree); + latexAreaTree.setClassName(FIELD_CLASS); + latexAreaUnification.setValue(latexCodeUnification + .replaceAll(Pattern.quote(LatexCreatorConstants.SUBSTITUTION_SIGN), RIGHT_ARROW_WHITE)); + latexAreaUnification.setClassName(FIELD_CLASS); UI.getCurrent().getPage().executeJs("window.autoSelect($0)", FIELD_CLASS); setReadOnly(); - layout.add(urlField, packageArea, latexArea); + layout.add(urlField, packageAreaTree, latexAreaTree, packageAreaUnification, latexAreaUnification); add(headingLayout, layout); } @@ -79,13 +93,17 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver { public void localeChange(LocaleChangeEvent localeChangeEvent) { heading.setText(getTranslation("share.heading")); urlField.setLabel(getTranslation("share.url.label")); - packageArea.setLabel(getTranslation("share.packages.label")); - latexArea.setLabel(getTranslation("share.latex.label")); + packageAreaTree.setLabel(getTranslation("share.packagesTree.label")); + latexAreaTree.setLabel(getTranslation("share.latexTree.label")); + packageAreaUnification.setLabel(getTranslation("share.packagesUnification.label")); + latexAreaUnification.setLabel(getTranslation("share.latexUnification.label")); } private void setReadOnly() { urlField.setReadOnly(true); - packageArea.setReadOnly(true); - latexArea.setReadOnly(true); + packageAreaTree.setReadOnly(true); + latexAreaTree.setReadOnly(true); + packageAreaUnification.setReadOnly(true); + latexAreaUnification.setReadOnly(true); } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index 8cd53c3..164f10d 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java @@ -124,7 +124,10 @@ public class TypeInferenceView extends VerticalLayout @Override public void shareButton() { UI.getCurrent().getPage().executeJs("return decodeURI(window.location.href)").then(url -> - new ShareDialog(url.asString().replace(" ", "%20"), lc.getTree()).open() + new ShareDialog( + url.asString().replace(" ", "%20"), + lc.getTree(), + lc.getUnification()[currentStep]).open() ); } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java index e695a17..381a731 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java @@ -9,6 +9,12 @@ public final class LatexCreatorConstants { private LatexCreatorConstants() { } + /** + * needs to be replaced to be compatible with normal LaTeX + */ + public static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}"; + + protected static final String CONST = "Const"; protected static final String LET = "let"; protected static final String IN = "in"; @@ -52,7 +58,6 @@ public final class LatexCreatorConstants { protected static final String LATEX_NEW_LINE = "\\\\"; protected static final String CIRC = "\\circ"; - protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}"; protected static final String COLOR_RED = "\\color{#f00}"; protected static final String COLOR_HIGHLIGHT = "\\color{#006AF5}"; protected static final String EMPTY_SET = "\\emptyset"; diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties index b7df9bd..4c56678 100644 --- a/src/main/resources/language/general.properties +++ b/src/main/resources/language/general.properties @@ -81,6 +81,10 @@ root.varLetLatex=\ \\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\ \\end{prooftree} -share.neededPackages=\ +share.neededPackagesTree=\ \\usepackage{bussproofs}\n\ -\\usepackage{amsmath} \ No newline at end of file +\\usepackage{amsmath} +share.neededPackagesUnification=\ +\\usepackage{amsmath}\ +\\usepackage{xcolor}\ +\\usepackage{stix} \ No newline at end of file diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index e2bc22c..5389e10 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -153,5 +153,7 @@ root.different_types = Der eingegebene Term ist nicht typisierbar: \ share.heading=Teilen share.url.label=URL -share.packages.label=Pakete -share.latex.label=LaTeX-Code +share.packagesTree.label=Pakete (Typherleitungsbaum) +share.latexTree.label=LaTeX-Code (Typherleitungsbaum) +share.packagesUnification.label=Pakete (Unifikation/MGU) +share.latexUnification.label=LaTeX-Code (Unifikation/MGU) diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties index a90cef6..808ece2 100644 --- a/src/main/resources/language/translation_en.properties +++ b/src/main/resources/language/translation_en.properties @@ -145,5 +145,7 @@ root.different_types = The entered term cannot be typed: \ share.heading=Share share.url.label=URL -share.packages.label=Packages -share.latex.label=LaTeX code +share.packagesTree.label=Packages (inference tree) +share.latexTree.label=LaTeX code (inference tree) +share.packagesUnification.label=Packages (unification/MGU) +share.latexUnification.label=LaTeX code (unifcation/MgU)