mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
a4f3b38a10
@ -33,12 +33,16 @@
|
|||||||
align-items: center;
|
align-items: center;
|
||||||
}
|
}
|
||||||
|
|
||||||
pre {
|
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;
|
display: inline-block;
|
||||||
padding-left: 0.2em;
|
font-size: .85em;
|
||||||
padding-right: 0.2em;
|
font-weight: 700;
|
||||||
}
|
line-height: 1;
|
||||||
|
padding: 2px 4px;
|
||||||
div {
|
white-space: nowrap;
|
||||||
margin: 0;
|
|
||||||
}
|
}
|
@ -1,16 +1,13 @@
|
|||||||
package edu.kit.typicalc.view.main;
|
package edu.kit.typicalc.view.main;
|
||||||
|
|
||||||
import com.vaadin.flow.component.Component;
|
|
||||||
import com.vaadin.flow.component.ItemLabelGenerator;
|
import com.vaadin.flow.component.ItemLabelGenerator;
|
||||||
import com.vaadin.flow.component.UI;
|
import com.vaadin.flow.component.UI;
|
||||||
import com.vaadin.flow.component.accordion.Accordion;
|
import com.vaadin.flow.component.accordion.Accordion;
|
||||||
import com.vaadin.flow.component.button.Button;
|
import com.vaadin.flow.component.button.Button;
|
||||||
import com.vaadin.flow.component.dependency.CssImport;
|
import com.vaadin.flow.component.dependency.CssImport;
|
||||||
import com.vaadin.flow.component.dialog.Dialog;
|
import com.vaadin.flow.component.dialog.Dialog;
|
||||||
import com.vaadin.flow.component.html.Div;
|
|
||||||
import com.vaadin.flow.component.html.H3;
|
import com.vaadin.flow.component.html.H3;
|
||||||
import com.vaadin.flow.component.html.Pre;
|
import com.vaadin.flow.component.html.Paragraph;
|
||||||
import com.vaadin.flow.component.html.Span;
|
|
||||||
import com.vaadin.flow.component.icon.Icon;
|
import com.vaadin.flow.component.icon.Icon;
|
||||||
import com.vaadin.flow.component.icon.VaadinIcon;
|
import com.vaadin.flow.component.icon.VaadinIcon;
|
||||||
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
|
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
|
||||||
@ -40,6 +37,7 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
private final H3 heading;
|
private final H3 heading;
|
||||||
private final Select<Locale> languageSelect;
|
private final Select<Locale> languageSelect;
|
||||||
private final ItemLabelGenerator<Locale> renderer;
|
private final ItemLabelGenerator<Locale> renderer;
|
||||||
|
private final Paragraph shortcuts;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Create a new HelpDialog.
|
* Create a new HelpDialog.
|
||||||
@ -48,6 +46,7 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
HorizontalLayout headingLayout = new HorizontalLayout();
|
HorizontalLayout headingLayout = new HorizontalLayout();
|
||||||
renderer = item -> getTranslation("root." + item.getDisplayLanguage(Locale.ENGLISH).toLowerCase());
|
renderer = item -> getTranslation("root." + item.getDisplayLanguage(Locale.ENGLISH).toLowerCase());
|
||||||
heading = new H3();
|
heading = new H3();
|
||||||
|
shortcuts = new Paragraph();
|
||||||
headingLayout.setId(HEADING_LAYOUT_ID);
|
headingLayout.setId(HEADING_LAYOUT_ID);
|
||||||
|
|
||||||
languageSelect = new Select<>(Locale.GERMAN, Locale.ENGLISH);
|
languageSelect = new Select<>(Locale.GERMAN, Locale.ENGLISH);
|
||||||
@ -75,7 +74,7 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
acc.add(new HelpContentField("root.typeInferButton", "root.helpTypeInferButton"));
|
acc.add(new HelpContentField("root.typeInferButton", "root.helpTypeInferButton"));
|
||||||
acc.add(new HelpContentField("root.inputField", "root.helpInputField"));
|
acc.add(new HelpContentField("root.inputField", "root.helpInputField"));
|
||||||
acc.add(new HelpContentField("root.typeAssumptions", "root.helpTypeAssumptions"));
|
acc.add(new HelpContentField("root.typeAssumptions", "root.helpTypeAssumptions"));
|
||||||
acc.add(new HelpContentField("root.shortcuts", createShortcutComponent()));
|
acc.add(new HelpContentField("root.shortcuts", shortcuts));
|
||||||
acc.add(new HelpContentField("root.drawer",
|
acc.add(new HelpContentField("root.drawer",
|
||||||
new Button(new Icon(VaadinIcon.MENU)), "root.helpDrawer"));
|
new Button(new Icon(VaadinIcon.MENU)), "root.helpDrawer"));
|
||||||
acc.add(new HelpContentField("root.example",
|
acc.add(new HelpContentField("root.example",
|
||||||
@ -93,30 +92,10 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
return acc;
|
return acc;
|
||||||
}
|
}
|
||||||
|
|
||||||
private Component createShortcutComponent() {
|
|
||||||
VerticalLayout layout = new VerticalLayout();
|
|
||||||
layout.add(new Div(
|
|
||||||
new Span(getTranslation("root.shortcut0")),
|
|
||||||
new Pre(getTranslation("root.shortcut0key"))));
|
|
||||||
layout.add(new Div(
|
|
||||||
new Span(getTranslation("root.shortcut1")),
|
|
||||||
new Pre(getTranslation("root.shortcut1key"))));
|
|
||||||
layout.add(new Div(
|
|
||||||
new Span(getTranslation("root.shortcut2")),
|
|
||||||
new Pre(getTranslation("root.shortcut2key"))));
|
|
||||||
layout.add(new Div(
|
|
||||||
new Span(getTranslation("root.shortcut3")),
|
|
||||||
new Pre(getTranslation("root.shortcut3key"))));
|
|
||||||
layout.add(new Div(
|
|
||||||
new Span(getTranslation("root.shortcut4")),
|
|
||||||
new Pre(getTranslation("root.shortcut4key"))));
|
|
||||||
// TODO: localeChange, English translation texts
|
|
||||||
return layout;
|
|
||||||
}
|
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void localeChange(LocaleChangeEvent event) {
|
public void localeChange(LocaleChangeEvent event) {
|
||||||
heading.setText(getTranslation("root.operatingHelp"));
|
heading.setText(getTranslation("root.operatingHelp"));
|
||||||
|
shortcuts.getElement().setProperty("innerHTML", getTranslation("root.helpShortcuts"));
|
||||||
languageSelect.setLabel(getTranslation("root.selectLanguage"));
|
languageSelect.setLabel(getTranslation("root.selectLanguage"));
|
||||||
languageSelect.setTextRenderer(renderer);
|
languageSelect.setTextRenderer(renderer);
|
||||||
}
|
}
|
||||||
|
@ -52,6 +52,11 @@ automatisch zu einer Typvariable.
|
|||||||
root.helpTypeInferButton=Durch Benutzen des Typisieren-Knopfs wird die Berechnung des Typinferenzalgorithmus mit \
|
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 \
|
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.
|
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. \
|
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 \
|
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 \
|
Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Benutzen des Knopfs \
|
||||||
@ -70,16 +75,6 @@ root.helpShareButton=Durch Benutzen des Teilen-Knopfs öffnet sich ein Dialog, i
|
|||||||
Typherleitungsbaums des eingegebenen Terms und die benötigen Pakete zum Einbinden des LaTeX-Codes angezeigt werden. \
|
Typherleitungsbaums des eingegebenen Terms und die benötigen Pakete zum Einbinden des LaTeX-Codes angezeigt werden. \
|
||||||
Zusätzlich dazu enthält der Dialog einen Permalink zur aktuellen Seite, der sowohl den Term als auch die Typannahmen \
|
Zusätzlich dazu enthält der Dialog einen Permalink zur aktuellen Seite, der sowohl den Term als auch die Typannahmen \
|
||||||
kodiert.
|
kodiert.
|
||||||
root.shortcut0=Fokus auf Eingabefeld:
|
|
||||||
root.shortcut0key=/⃣
|
|
||||||
root.shortcut1=Erster Schritt: Strg +
|
|
||||||
root.shortcut1key=←⃣
|
|
||||||
root.shortcut2=Vorheriger Schritt:
|
|
||||||
root.shortcut2key=←⃣
|
|
||||||
root.shortcut3=Nächster Schritt:
|
|
||||||
root.shortcut3key=→⃣
|
|
||||||
root.shortcut4=Letzter Schritt: Strg +
|
|
||||||
root.shortcut4key=→⃣
|
|
||||||
root.TOO_FEW_TOKENS=Falsche Eingabe! Der Term endet abrupt.
|
root.TOO_FEW_TOKENS=Falsche Eingabe! Der Term endet abrupt.
|
||||||
root.tooFewTokensHelp=Überprüfe, ob alle Let-, Abs- und App-Terme über die nötigen Argumente verfügen.
|
root.tooFewTokensHelp=Überprüfe, ob alle Let-, Abs- und App-Terme über die nötigen Argumente verfügen.
|
||||||
root.UNEXPECTED_TOKEN=Der Term entspricht nicht der im Info-Dialog spezifizierten Syntax!
|
root.UNEXPECTED_TOKEN=Der Term entspricht nicht der im Info-Dialog spezifizierten Syntax!
|
||||||
|
@ -50,6 +50,11 @@ converted to a type variable.
|
|||||||
root.helpTypeInferButton=Clicking on the type button starts the type inference algorithm for the current input. \
|
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 \
|
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.
|
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. \
|
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 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 \
|
If the unification algorithm is already in progress, clicking on the button shows the last step of the inference \
|
||||||
|
Loading…
Reference in New Issue
Block a user