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

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
Moritz Dieing 2021-03-05 17:11:23 +01:00
commit ca2b3ac934
16 changed files with 183 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
frontend/styles/view/main/example-dialog.css Normal file
View File

@ -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;
}

20
frontend/styles/view/main/help-dialog.css
View File

@ -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;
}

14
frontend/styles/view/main/type-assumptions-area.css
View File

@ -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;

14
frontend/styles/view/share-dialog.css
View File

@ -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;
}

40
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java
View File

@ -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&ltpackage&gt“
* @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"));
}
}

2
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java
View File

@ -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()
);
}

13
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
View File

@ -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

2
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java
View File

@ -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}";
}

22
src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
View File

@ -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<String> 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);
}

24
src/main/java/edu/kit/typicalc/view/main/HelpContentField.java
View File

@ -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));
}

31
src/main/java/edu/kit/typicalc/view/main/HelpDialog.java
View File

@ -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<Locale> languageSelect;
private final ItemLabelGenerator<Locale> 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);
}
}

2
src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java
View File

@ -95,7 +95,7 @@ public class MainViewImpl extends AppLayout
private void setTermInURL(Pair<String, Map<String, String>> 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;
}

18
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java
View File

@ -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.
*/

16
src/main/resources/language/general.properties
View File

@ -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}
share.neededPackages=\
\\usepackage{bussproofs}\n\
\\usepackage{amsmath}

6
src/main/resources/language/translation_de.properties
View File

@ -26,6 +26,7 @@ root.title404=404 - Seite nicht gefunden
root.message404=Versuche /infer/<term> 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=<kbd>Strg</kbd> + <kbd>\u2190</kbd> = Erster Schritt<br>\
<kbd>\u2190</kbd> = Vorheriger Schritt<br>\
<kbd>\u2192</kbd> = Nächster Schritt<br>\
<kbd>Strg</kbd> + <kbd>\u2192</kbd> = Letzter Schritt<br>\
<kbd>/</kbd> = 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 \

6
src/main/resources/language/translation_en.properties
View File

@ -26,6 +26,7 @@ root.title404=404 - Not Found
root.message404=Try /infer/<term> 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=<kbd>Ctrl</kbd> + <kbd>\u2190</kbd> = First step<br>\
<kbd>\u2190</kbd> = Previous step<br>\
<kbd>\u2192</kbd> = Next step<br>\
<kbd>Ctrl</kbd> + <kbd>\u2192</kbd> = Last step<br>\
<kbd>/</kbd> = 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 \