diff --git a/frontend/styles/view/main/example-dialog.css b/frontend/styles/view/main/example-dialog.css new file mode 100644 index 0000000..234a86f --- /dev/null +++ b/frontend/styles/view/main/example-dialog.css @@ -0,0 +1,13 @@ +#headingLayout { + width: 100%; + display: flex; + position: relative; + align-items: center; + justify-content: center; +} + +#closeIcon { + right: 0; + position: absolute; + bottom: 2.1em; +} \ No newline at end of file diff --git a/frontend/styles/view/main/help-dialog.css b/frontend/styles/view/main/help-dialog.css index 1129295..b1c21b3 100644 --- a/frontend/styles/view/main/help-dialog.css +++ b/frontend/styles/view/main/help-dialog.css @@ -22,11 +22,27 @@ width: 100%; } -#typeButtonCopy { - min-width: 110px; +#closeIcon { + right: 0; + position: absolute; + bottom: 2.1em; } .help-field { justify-content: center; align-items: center; +} + +kbd { + background-color: #eee; + border-radius: 3px; + border: 1px solid #b4b4b4; + box-shadow: 0 1px 1px rgba(0, 0, 0, .2), 0 2px 0 0 rgba(255, 255, 255, .7) inset; + color: #333; + display: inline-block; + font-size: .85em; + font-weight: 700; + line-height: 1; + padding: 2px 4px; + white-space: nowrap; } \ No newline at end of file diff --git a/frontend/styles/view/main/type-assumptions-area.css b/frontend/styles/view/main/type-assumptions-area.css index f78e02b..e603e17 100644 --- a/frontend/styles/view/main/type-assumptions-area.css +++ b/frontend/styles/view/main/type-assumptions-area.css @@ -5,6 +5,20 @@ padding: 0; } +#headingLayout { + width: 100%; + display: flex; + position: relative; + align-items: center; + justify-content: center; +} + +#closeIcon { + right: 0; + position: absolute; + bottom: 2.1em; +} + #assButtons { display: flex; justify-content: center; diff --git a/frontend/styles/view/share-dialog.css b/frontend/styles/view/share-dialog.css index 6812a99..f306841 100644 --- a/frontend/styles/view/share-dialog.css +++ b/frontend/styles/view/share-dialog.css @@ -9,3 +9,17 @@ .share-dialog-field { width: 100%; } + +#headingLayout { + width: 100%; + display: flex; + position: relative; + align-items: center; + justify-content: center; +} + +#closeIcon { + right: 0; + position: absolute; + bottom: 2.1em; +} 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 6805212..5b5df8a 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 @@ -3,6 +3,9 @@ package edu.kit.typicalc.view.content.typeinferencecontent; import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H3; +import com.vaadin.flow.component.icon.Icon; +import com.vaadin.flow.component.icon.VaadinIcon; +import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.component.textfield.TextArea; import com.vaadin.flow.component.textfield.TextField; @@ -15,12 +18,14 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; @CssImport("./styles/view/share-dialog.css") public class ShareDialog extends Dialog implements LocaleChangeObserver { + private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String SHARE_DIALOG_ID = "shareDialog"; private static final String LAYOUT_ID = "share-dialog-layout"; private static final String FIELD_CLASS = "share-dialog-field"; + private static final String CLOSE_ICON_ID = "closeIcon"; private final TextField urlField; - private final TextField packageField; + private final TextArea packageArea; private final TextArea latexArea; private final H3 heading; @@ -29,29 +34,38 @@ 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 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) */ - public ShareDialog(String url, String latexPackages, String latexCode) { - VerticalLayout layout = new VerticalLayout(); - layout.setId(LAYOUT_ID); - add(layout); - setId(SHARE_DIALOG_ID); + public ShareDialog(String url, String latexCode) { + HorizontalLayout headingLayout = new HorizontalLayout(); + headingLayout.setId(HEADING_LAYOUT_ID); heading = new H3(); + Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL); + closeIcon.addClickListener(event -> this.close()); + closeIcon.setId(CLOSE_ICON_ID); + + headingLayout.add(heading); + headingLayout.add(closeIcon); + + VerticalLayout layout = new VerticalLayout(); + layout.setId(LAYOUT_ID); + setId(SHARE_DIALOG_ID); + urlField = new TextField(); - packageField = new TextField(); + packageArea = new TextArea(); latexArea = new TextArea(); urlField.setValue(url); urlField.setClassName(FIELD_CLASS); - packageField.setValue(latexPackages); - packageField.setClassName(FIELD_CLASS); + packageArea.setValue(getTranslation("share.neededPackages")); + packageArea.setClassName(FIELD_CLASS); latexArea.setValue(latexCode); latexArea.setClassName(FIELD_CLASS); - layout.add(heading, urlField, packageField, latexArea); + layout.add(urlField, packageArea, latexArea); + + add(headingLayout, layout); } @@ -59,7 +73,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver { public void localeChange(LocaleChangeEvent localeChangeEvent) { heading.setText(getTranslation("share.heading")); urlField.setLabel(getTranslation("share.url.label")); - packageField.setLabel(getTranslation("share.packages.label")); + packageArea.setLabel(getTranslation("share.packages.label")); latexArea.setLabel(getTranslation("share.latex.label")); } } 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 f189547..5136e5a 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 @@ -82,7 +82,7 @@ public class TypeInferenceView extends VerticalLayout @Override public void shareButton() { 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() ); } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java index 0027bca..e841c98 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java @@ -77,16 +77,6 @@ public class LatexCreator implements StepVisitor { 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) { String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions()); String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex(); @@ -155,8 +145,7 @@ public class LatexCreator implements StepVisitor { tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC)); String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise()); String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex(); - String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType - + DOLLAR_SIGN + NEW_LINE; + String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType + DOLLAR_SIGN; String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN + generateVarStepPremise(varL).replace(DOLLAR_SIGN, "") + SPACE + LATEX_NEW_LINE + SPACE // todo less replacement fixups 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 a24e587..0a1e65c 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 @@ -74,6 +74,4 @@ public final class LatexCreatorConstants { protected static final String ALIGN_END = "\\end{aligned}"; protected static final String SPLIT_BEGIN = "\\begin{split}"; protected static final String SPLIT_END = "\\end{split}"; - - protected static final String BUSSPROOFS = "\\usepackage{bussproofs}"; } diff --git a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java index d53b970..023213a 100644 --- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java @@ -1,8 +1,12 @@ package edu.kit.typicalc.view.main; import com.vaadin.flow.component.button.Button; +import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H3; +import com.vaadin.flow.component.icon.Icon; +import com.vaadin.flow.component.icon.VaadinIcon; +import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; @@ -13,11 +17,14 @@ import java.util.function.Consumer; * Contains all predefined examples as buttons. * Clicking on a button inserts the example string into the input field. */ +@CssImport("./styles/view/main/example-dialog.css") public class ExampleDialog extends Dialog implements LocaleChangeObserver { private static final long serialVersionUID = 8718432784530464215L; + private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String EXAMPLE_DIALOG_ID = "exampleDialog"; + private static final String CLOSE_ICON_ID = "closeIcon"; private final H3 instruction; @@ -27,10 +34,19 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver { * @param callback function to handle the selected lambda term */ protected ExampleDialog(Consumer callback) { + instruction = new H3(); + HorizontalLayout headingLayout = new HorizontalLayout(); + headingLayout.setId(HEADING_LAYOUT_ID); + + Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL); + closeIcon.addClickListener(event -> this.close()); + closeIcon.setId(CLOSE_ICON_ID); + + headingLayout.add(instruction); + headingLayout.add(closeIcon); + String[] examples = getTranslation("root.exampleTerms").split(","); VerticalLayout layout = new VerticalLayout(); - instruction = new H3(); - layout.add(instruction); for (String term : examples) { Button button = new Button(term); button.addClickListener(click -> { @@ -40,7 +56,7 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver { button.setId(term); // needed for integration test layout.add(button); } - add(layout); + add(headingLayout, layout); setId(EXAMPLE_DIALOG_ID); } diff --git a/src/main/java/edu/kit/typicalc/view/main/HelpContentField.java b/src/main/java/edu/kit/typicalc/view/main/HelpContentField.java index 36185cf..8a843b2 100644 --- a/src/main/java/edu/kit/typicalc/view/main/HelpContentField.java +++ b/src/main/java/edu/kit/typicalc/view/main/HelpContentField.java @@ -1,9 +1,11 @@ package edu.kit.typicalc.view.main; +import com.vaadin.flow.component.Component; import com.vaadin.flow.component.accordion.AccordionPanel; import com.vaadin.flow.component.button.Button; import com.vaadin.flow.component.details.DetailsVariant; import com.vaadin.flow.component.html.Paragraph; +import com.vaadin.flow.component.orderedlayout.FlexComponent; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; @@ -19,6 +21,8 @@ public class HelpContentField extends AccordionPanel implements LocaleChangeObse private final String summaryKey; private final String contentKey; + private final HorizontalLayout summary; + private final Paragraph summaryText; private final Paragraph content; /** @@ -30,8 +34,11 @@ public class HelpContentField extends AccordionPanel implements LocaleChangeObse protected HelpContentField(String summaryKey, String contentKey) { this.summaryKey = summaryKey; this.contentKey = contentKey; - this.content = new Paragraph(getTranslation(contentKey)); - setSummaryText(getTranslation(summaryKey)); + this.content = new Paragraph(); + this.summaryText = new Paragraph(); + this.summary = new HorizontalLayout(summaryText); + summary.setAlignItems(FlexComponent.Alignment.BASELINE); + setSummary(summary); setContent(content); addThemeVariants(DetailsVariant.FILLED); } @@ -46,14 +53,19 @@ public class HelpContentField extends AccordionPanel implements LocaleChangeObse */ protected HelpContentField(String summaryKey, Button button, String contentKey) { this(summaryKey, contentKey); - HorizontalLayout layout = new HorizontalLayout(button, content); - layout.setClassName(CLASSNAME); - setContent(layout); + summary.removeAll(); + summary.add(button, summaryText); + setContent(content); + } + + protected HelpContentField(String summaryKey, Component contentComponent) { + this(summaryKey, ""); + setContent(contentComponent); } @Override public void localeChange(LocaleChangeEvent event) { - setSummaryText(getTranslation(summaryKey)); + summaryText.setText(getTranslation(summaryKey)); content.setText(getTranslation(contentKey)); } diff --git a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java index e66481a..3bd0d88 100644 --- a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java @@ -3,12 +3,11 @@ package edu.kit.typicalc.view.main; import com.vaadin.flow.component.ItemLabelGenerator; import com.vaadin.flow.component.UI; import com.vaadin.flow.component.accordion.Accordion; -import com.vaadin.flow.component.applayout.DrawerToggle; import com.vaadin.flow.component.button.Button; -import com.vaadin.flow.component.button.ButtonVariant; import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H3; +import com.vaadin.flow.component.html.Paragraph; import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.VaadinIcon; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; @@ -33,12 +32,12 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver { private static final String CONTENT_LAYOUT_ID = "contentLayout"; private static final String LANGUAGE_SELECT_ID = "languageSelect"; private static final String ACCORDION_ID = "accordion"; - private static final String TYPE_BUTTON_COPY_ID = "typeButtonCopy"; + private static final String CLOSE_ICON_ID = "closeIcon"; private final H3 heading; private final Select languageSelect; private final ItemLabelGenerator renderer; - private final Button typeButtonCopy; + private final Paragraph shortcuts; /** * Create a new HelpDialog. @@ -47,18 +46,22 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver { HorizontalLayout headingLayout = new HorizontalLayout(); renderer = item -> getTranslation("root." + item.getDisplayLanguage(Locale.ENGLISH).toLowerCase()); heading = new H3(); + shortcuts = new Paragraph(); headingLayout.setId(HEADING_LAYOUT_ID); + languageSelect = new Select<>(Locale.GERMAN, Locale.ENGLISH); languageSelect.setTextRenderer(renderer); languageSelect.setValue(UI.getCurrent().getLocale()); languageSelect.addValueChangeListener(event -> UI.getCurrent().getSession().setLocale(event.getValue())); languageSelect.setId(LANGUAGE_SELECT_ID); - headingLayout.add(heading, languageSelect); + + Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL); + closeIcon.addClickListener(event -> this.close()); + closeIcon.setId(CLOSE_ICON_ID); + + headingLayout.add(heading, languageSelect, closeIcon); VerticalLayout contentLayout = new VerticalLayout(); - typeButtonCopy = new Button(getTranslation("root.typeInfer")); - typeButtonCopy.addThemeVariants(ButtonVariant.LUMO_PRIMARY); - typeButtonCopy.setId(TYPE_BUTTON_COPY_ID); Accordion content = createHelpContent(); content.setId(ACCORDION_ID); contentLayout.add(content); @@ -68,12 +71,14 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver { private Accordion createHelpContent() { Accordion acc = new Accordion(); - acc.add(new HelpContentField("root.drawer", new DrawerToggle(), "root.helpDrawer")); - acc.add(new HelpContentField("root.example", - new Button(getTranslation("root.examplebutton")), "root.helpExample")); + acc.add(new HelpContentField("root.typeInferButton", "root.helpTypeInferButton")); acc.add(new HelpContentField("root.inputField", "root.helpInputField")); acc.add(new HelpContentField("root.typeAssumptions", "root.helpTypeAssumptions")); - acc.add(new HelpContentField("root.typeInferButton", typeButtonCopy, "root.helpTypeInferButton")); + acc.add(new HelpContentField("root.shortcuts", shortcuts)); + acc.add(new HelpContentField("root.drawer", + new Button(new Icon(VaadinIcon.MENU)), "root.helpDrawer")); + acc.add(new HelpContentField("root.example", + new Button(new Icon(VaadinIcon.PAPERCLIP)), "root.helpExample")); acc.add(new HelpContentField("root.firstStepButton", new Button(new Icon(VaadinIcon.ANGLE_DOUBLE_LEFT)), "root.helpFirstStepButton")); acc.add(new HelpContentField("root.previousStepButton", @@ -90,8 +95,8 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver { @Override public void localeChange(LocaleChangeEvent event) { heading.setText(getTranslation("root.operatingHelp")); + shortcuts.getElement().setProperty("innerHTML", getTranslation("root.helpShortcuts")); languageSelect.setLabel(getTranslation("root.selectLanguage")); - typeButtonCopy.setText(getTranslation("root.typeInfer")); languageSelect.setTextRenderer(renderer); } } diff --git a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java index 920dd5f..870d953 100644 --- a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java +++ b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java @@ -95,7 +95,7 @@ public class MainViewImpl extends AppLayout private void setTermInURL(Pair> lambdaTermAndAssumptions) { String lambdaTerm = lambdaTermAndAssumptions.getLeft(); if ("".equals(lambdaTerm)) { - UI.getCurrent().getPage().getHistory().pushState(null, new Location("")); + UI.getCurrent().getPage().getHistory().pushState(null, "./"); setContent(new StartPageView()); return; } diff --git a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java index 79f6bb6..95ca760 100644 --- a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java +++ b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java @@ -32,9 +32,11 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver /* * IDs for the imported .css-file */ + private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String ASS_LAYOUT_ID = "assLayout"; private static final String ASS_BUTTONS_ID = "assButtons"; private static final String ASS_CONTAINER_ID = "assContainer"; + private static final String CLOSE_ICON_ID = "closeIcon"; private final H3 heading; private final VerticalLayout assumptionContainer; @@ -71,8 +73,9 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver assumptionContainer.setId(ASS_CONTAINER_ID); initializeWithAssumptions(types); - layout.add(heading, buttons, assumptionContainer); - add(layout); + layout.add(buttons, assumptionContainer); + HorizontalLayout headingLayout = makeHeader(); + add(headingLayout, layout); // attach and trigger javascript event listener after reopening the dialog addOpenedChangeListener(e -> { if (e.isOpened()) { @@ -82,6 +85,17 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver ); } + private HorizontalLayout makeHeader() { + HorizontalLayout headingLayout = new HorizontalLayout(); + headingLayout.setId(HEADING_LAYOUT_ID); + + Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL); + closeIcon.addClickListener(event -> this.close()); + closeIcon.setId(CLOSE_ICON_ID); + headingLayout.add(heading); + headingLayout.add(closeIcon); + return headingLayout; + } /** * Creates a new empty TypeAssumptionsArea. */ diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties index 001381c..b7df9bd 100644 --- a/src/main/resources/language/general.properties +++ b/src/main/resources/language/general.properties @@ -33,7 +33,7 @@ root.appLatex=\ \ \\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\ \ -\\LeftLabel{\\rm A{\\small PP}}\ +\\LeftLabel{\\textrm A{\\small PP}}\ \\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\ \\end{prooftree} @@ -41,7 +41,7 @@ root.absLatex=\ \\begin{prooftree}\ \\AxiomC{$\\Gamma , \\texttt{x}: \\tau_1 \\vdash t : \\tau_2$}\ \ -\\LeftLabel{\\rm A{\\small BS}}\ +\\LeftLabel{\\textrm A{\\small BS}}\ \\UnaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\ \\end{prooftree} @@ -49,7 +49,7 @@ root.varLatex=\ \\begin{prooftree}\ \\AxiomC{$\\Gamma (\\texttt{x}) = \\tau$}\ \ -\\LeftLabel{\\rm V{\\small AR}}\ +\\LeftLabel{\\textrm V{\\small AR}}\ \\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau'$}\ \\end{prooftree} @@ -57,7 +57,7 @@ root.constLatex=\ \\begin{prooftree}\ \\AxiomC{$\\texttt{c} \\in Const$}\ \ -\\LeftLabel{\\rm C{\\small ONST}}\ +\\LeftLabel{\\textrm C{\\small ONST}}\ \\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau_c$}\ \\end{prooftree} @@ -67,7 +67,7 @@ root.letLatex=\ \ \\AxiomC{$\\Gamma , \\texttt{x} : ta(\\tau_1 , \\Gamma ) \\vdash t_2 : \\tau_2$}\ \ -\\LeftLabel{\\rm L{\\small ET}}\ +\\LeftLabel{\\textrm L{\\small ET}}\ \\BinaryInfC{$\\Gamma \\vdash \\textbf{let} \\ \\texttt{x} = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\ \\end{prooftree} @@ -77,6 +77,10 @@ root.varLetLatex=\ \ \\AxiomC{$\\tau' \\succeq \\tau$}\ \ -\\LeftLabel{\\rm V{\\small AR}}\ +\\LeftLabel{\\textrm V{\\small AR}}\ \\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\ -\\end{prooftree} \ No newline at end of file +\\end{prooftree} + +share.neededPackages=\ +\\usepackage{bussproofs}\n\ +\\usepackage{amsmath} \ 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 b074a6c..f8c5e9f 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -26,6 +26,7 @@ root.title404=404 - Seite nicht gefunden root.message404=Versuche /infer/ oder gebe deinen Lieblingsterm in das Eingabefeld ein root.drawer=Drawer (Ableitungsregeln) root.example=Beispiele +root.shortcuts=Tastaturbefehle root.inputField=Eingabefeld root.typeInferButton=Typisieren-Knopf root.firstStepButton=Erster-Schritt-Knopf @@ -51,6 +52,11 @@ automatisch zu einer Typvariable. root.helpTypeInferButton=Durch Benutzen des Typisieren-Knopfs wird die Berechnung des Typinferenzalgorithmus mit \ der aktuellen Eingabe gestartet. Je größer der Term desto länger dauert das Anzeigen des Typherleitungsbaums. Bei sehr \ großer Eingabe oder einem langsamen Rechner wird also etwas Geduld benötigt. +root.helpShortcuts=Strg + \u2190 = Erster Schritt
\ +\u2190 = Vorheriger Schritt
\ +\u2192 = Nächster Schritt
\ +Strg + \u2192 = Letzter Schritt
\ +/ = Fokus auf Eingabefeld root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funktion des Knopfs. \ Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Benutzen des Knopfs zurück zum ersten Schritt des \ Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Benutzen des Knopfs \ diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties index a006223..817cbf7 100644 --- a/src/main/resources/language/translation_en.properties +++ b/src/main/resources/language/translation_en.properties @@ -26,6 +26,7 @@ root.title404=404 - Not Found root.message404=Try /infer/ or type your favourite term into the input field root.drawer=Drawer (type inference rules) root.example=Examples +root.shortcuts=Shortcuts root.inputField=Input Field root.typeInferButton=Type Button root.firstStepButton=First-Step Button @@ -49,6 +50,11 @@ converted to a type variable. root.helpTypeInferButton=Clicking on the type button starts the type inference algorithm for the current input. \ The longer the entered term the longer the time to display the type inference tree. With a slow computer or a \ very long term a lot of patience will be required. +root.helpShortcuts=Ctrl + \u2190 = First step
\ +\u2190 = Previous step
\ +\u2192 = Next step
\ +Ctrl + \u2192 = Last step
\ +/ = Focus input bar root.helpFirstStepButton=The function of the button depends on the current state of the algorithm. \ If the tree is currently being built up, clicking on the button shows the first step of the inference tree. \ If the unification algorithm is already in progress, clicking on the button shows the last step of the inference \