Extend language files

frontend/styles/view/main/inference-rule-field.css

@@ -27,4 +27,4 @@
 	width: 100%;
 	margin: 0px;
 	padding-top: 0.2em;
-}
+}

src/main/java/edu/kit/typicalc/view/main/DrawerContent.java

@@ -36,12 +36,14 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
     }
 
     private void initRuleContainer() {
-        //TODO just demo content, exchange with correct rules
-        ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
-        ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
-        ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
-        ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
-        ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
+        ruleContainer.add(new InferenceRuleField(getTranslation("root.absLatex"), "root.absRule"));
+        ruleContainer.add(new InferenceRuleField(getTranslation("root.appLatex"), "root.appRule"));
+        ruleContainer.add(new InferenceRuleField(getTranslation("root.varLatex"), "root.varRule"));
+        ruleContainer.add(new InferenceRuleField(getTranslation("root.constLatex"), "root.constRule"));
+        ruleContainer.add(new InferenceRuleField(getTranslation("root.letLatex"), "root.letRule"));
+        ruleContainer.add(new InferenceRuleField(getTranslation("root.absLetLatex"), "root.absRuleLet"));
+        ruleContainer.add(new InferenceRuleField(getTranslation("root.varLetLatex"), "root.varRuleLet"));
+
     }
 
     @Override

src/main/java/edu/kit/typicalc/view/main/UpperBar.java

@@ -10,6 +10,8 @@ import com.vaadin.flow.component.html.H1;
 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.i18n.LocaleChangeEvent;
+import com.vaadin.flow.i18n.LocaleChangeObserver;
 import com.vaadin.flow.router.Location;
 import edu.kit.typicalc.view.content.infocontent.StartPageView;
 import edu.kit.typicalc.view.main.MainView.MainViewListener;
@@ -23,7 +25,7 @@ import java.util.function.Consumer;
  * Contains all the components constantly shown in the upper part of the webage.
  */
 @CssImport("./styles/view/main/upper-bar.css")
-public class UpperBar extends HorizontalLayout {
+public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
     private static final long serialVersionUID = -7344967027514015830L;
 
     /*
@@ -101,4 +103,9 @@ public class UpperBar extends HorizontalLayout {
         Dialog helpDialog = new HelpDialog();
         helpDialog.open();
     }
+
+    @Override
+    public void localeChange(LocaleChangeEvent event) {
+       rules.setText(getTranslation("root.inferenceRules")); 
+    }
 }

src/main/resources/language/general.properties

@@ -1,2 +1,50 @@
 root.lambda=\u03BB
 root.home=home
+root.typicalc=Typicalc
+root.examplebutton=📂
+
+root.appLatex=\
+\\begin{prooftree}\
+\\AxiomC{$\\Gamma \\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\
+\
+\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\
+\
+\\LeftLabel{APP}\
+\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\
+\\end{prooftree}
+
+root.absLatex=\
+\\begin{prooftree}\
+\\AxiomC{$\\Gamma , x: \\tau_1 \\vdash t : \\tau_2$}\
+\
+\\LeftLabel{ABS}\
+\\UnaryInfC{$\\Gamma \\vdash \\lambda x.t : \\tau_1 \\rightarrow \\tau_2$}\
+\\end{prooftree}
+
+root.varLatex=\
+\\begin{prooftree}\
+\\AxiomC{$\\Gamma (x) = \\tau$}\
+\
+\\LeftLabel{VAR}\
+\\UnaryInfC{$\\Gamma \\vdash x : \\tau'$}\
+\\end{prooftree}
+
+root.letLatex=\
+\\begin{prooftree}\
+\\AxiomC{$\\Gamma \\vdash t_1 : \\tau_1$}\
+\
+\\AxiomC{$\\Gamma , x : ta(\\tau_1 , \\Gamma ) \\vdash t_2 : \\tau_2$}\
+\
+\\LeftLabel{APP}\
+\\BinaryInfC{$\\Gamma \\vdash\ \\textbf{let} \\ x = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\
+\\end{prooftree}
+
+root.varLetLatex=\
+\\begin{prooftree}\
+\\AxiomC{$\\Gamma (x) = \\tau'$}\
+\
+\\AxiomC{$\\tau' \\succeq \\tau$}\
+\
+\\LeftLabel{VAR}\
+\\BinaryInfC{$\\Gamma \\vdash x : \\tau$}\
+\\end{prooftree}

src/main/resources/language/translation_de.properties

@@ -1,23 +1,38 @@
 root.close=Schließen
 root.copyLatex=Kopiere Latex-Code
-root.typicalc=Typicalc
-root.examplebutton=📂
 root.selectExample=Beispiel auswählen:
 root.typeInfer=Typisieren
 root.operatingHelp=Bedienhilfen
 root.inputSyntax=Eingabe Syntax
 root.inferenceRules=Ableitungsregeln
-root.absRule=Abs-Regel
 root.overlongInput=Die maximale Länge der Eingabe beträgt 1000 Zeichen!
+root.absRule=Abs-Regel
+root.appRule=App-Regel
+root.varRule=Var-Regel
+root.constRule=Const-Regel
+root.letRule=Let-Regel
+root.absRuleLet=Abs-Regel mit Let
+root.varRuleLet=Var-Regel mit Let
+root.german=Deutsch
+root.english=Englisch
+root.selectLanguage=Sprache
 
-abs-rule=\
+root.constLatex=\
 \\begin{prooftree}\
-\\AxiomC{$\\Gamma \\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\
+\\AxiomC{\\texttt{c ist eine Konstante}}\
 \
-\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\
+\\LeftLabel{CONST}\
+\\UnaryInfC{$\\Gamma \\vdash c : \\tau_c$}\
+\\end{prooftree}
+
+root.absLetLatex=\
+\\begin{prooftree}\
+\\AxiomC{$\\Gamma , x: \\tau_1 \\vdash t : \\tau_2$}\
 \
-\\LeftLabel{APP}\
-\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\
+\\AxiomC{$\\tau_1$ \\ \\texttt{kein Typschema}}\
+\
+\\LeftLabel{ABS}\
+\\BinaryInfC{$\\Gamma \\vdash \\lambda x.t : \\tau_1 \\rightarrow \\tau_2$}\
 \\end{prooftree}
 
 demo-tree=\

src/main/resources/language/translation_en.properties

@@ -1,18 +1,38 @@
 root.close=Close
 root.copyLatex=Copy latex code
-root.typicalc=Typicalc
-root.examplebutton=📂
 root.selectExample=Select example:
-root.inferenceRules=Inference Rules
 root.typeInfer=Type
+root.operatingHelp=Operating Help
+root.inputSyntax=Input Syntax
+root.inferenceRules=Inference Rules
+root.overlongInput=The maximum input length is 1000 characters!
+root.absRule=Abs rule
+root.appRule=App rule
+root.varRule=Var rule
+root.constRule=Const rule
+root.letRule=Let rule
+root.absRuleLet=Abs rule with Let
+root.varRuleLet=Var rule with Let
+root.german=German
+root.english=English
+root.selectLanguage=Language
 
-abs-rule=\
-\\begin{prooftree}\n\
-\\AxiomC{$\\Gamma \\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\n\
-\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\n\
-\n\
-\\LeftLabel{APP}\n\
-\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\n\
+root.constLatex=\
+\\begin{prooftree}\
+\\AxiomC{\texttt{c is a constant}}\
+\
+\\LeftLabel{CONST}\
+\\UnaryInfC{$\\Gamma \\vdash c : \\tau_c$}\
+\\end{prooftree}
+
+root.absLetLatex=\
+\\begin{prooftree}\
+\\AxiomC{$\\Gamma , x: \\tau_1 \\vdash t : \\tau_2$}\
+\
+\\AxiomC{$\\tau_1$ \\ \\texttt{no type scheme}}\
+\
+\\LeftLabel{ABS}\
+\\BinaryInfC{$\\Gamma \\vdash \\lambda x.t : \\tau_1 \\rightarrow \\tau_2$}\
 \\end{prooftree}
 
 demo-tree=\