Update InfoDialog and HelpDialog

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

@@ -12,23 +12,26 @@ public class InfoContent extends VerticalLayout implements LocaleChangeObserver
     private final Span termExplanation;
     private final Paragraph termSyntax;
     private final Span assExplanation;
-    private final Paragraph assSyntax;
+    private final Span typeExplanation;
+    private final Paragraph typeSyntax;
 
     public InfoContent() {
         termExplanation = new Span();
         termSyntax = new Paragraph();
         assExplanation = new Span();
-        assSyntax = new Paragraph();
+        typeExplanation = new Span();
+        typeSyntax = new Paragraph();
         termSyntax.setId(GRAMMAR_ID);
-        assSyntax.setId(GRAMMAR_ID);
+        typeSyntax.setId(GRAMMAR_ID);
-        add(termExplanation, termSyntax, assExplanation, assSyntax);
+        add(termExplanation, termSyntax, assExplanation, typeExplanation, typeSyntax);
     }
 
     @Override
     public void localeChange(LocaleChangeEvent localeChangeEvent) {
         termExplanation.setText(getTranslation("root.termExplanation"));
         termSyntax.getElement().setProperty("innerHTML", getTranslation("root.termGrammar"));
-        assExplanation.setText(getTranslation("root.assExplanation"));
+        assExplanation.getElement().setProperty("innerHTML", getTranslation("root.assExplanation"));
-        assSyntax.getElement().setProperty("innerHTML", getTranslation("root.assGrammar"));
+        typeExplanation.setText(getTranslation("root.typeExplanation"));
+        typeSyntax.getElement().setProperty("innerHTML", getTranslation("root.typeGrammar"));
     }
 }

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

@@ -165,7 +165,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
         inferTypeButton.setText(getTranslation("root.typeInfer"));
         infoIcon.getElement().setAttribute("title", getTranslation("root.inputSyntax"));
         exampleButton.getElement().setAttribute("title", getTranslation("root.exampleTooltip"));
-        assumptionInputField.setPlaceholder("TODO"); // TODO replace with usefull placeholder
+        assumptionInputField.setPlaceholder(getTranslation("root.typeInputFieldPlaceholder"));
         assumptionInputField.setLabel(getTranslation("root.typeAssumptions"));
     }
 }

src/main/resources/language/general.properties

@@ -22,11 +22,13 @@ root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2
 \u2329Var\u232A ::= [a-zA-Z][a-zA-Z0-9]* <br> \
 \u2329Const\u232A ::= [0-9]+ | true | false
 
-root.assGrammar=\u2329Type\u232A ::= (\u2329Type\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \
+root.typeGrammar=\u2329Type\u232A ::= \u2329QuantifiedType\u232A | \u2329NormalType\u232A <br> \
+\u2329QuantifiedType\u232A ::= <b>∀</b>\u2329VarType\u232A<b>.</b>\u2329NormalType\u232A <br> \
+\u2329NormalType\u232A ::= (\u2329NormalType\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \
 \u2329FunctionType\u232A <br> \
 \u2329NamedType\u232A ::= [a-zA-Z][a-zA-Z0-9]*&nbsp;&nbsp\\t[0-9]+ <br> \
 \u2329VarType\u232A ::= t[0-9]+ <br> \
-\u2329FunctionType\u232A ::= \u2329Type\u232A -> \u2329Type\u232A
+\u2329FunctionType\u232A ::= \u2329NormalType\u232A -> \u2329NormalType\u232A
 
 root.appLatex=\
 \\begin{prooftree}\

src/main/resources/language/translation_de.properties

@@ -14,11 +14,15 @@ root.varRule=Var-Regel
 root.constRule=Const-Regel
 root.letRule=Let-Regel
 root.inputFieldPlaceholder=Term hier eingeben. Ein '\\' wird zu '\u03BB' umgewandelt.
+root.typeInputFieldPlaceholder=Typannahmen hier eingeben. Ein '!' wird zu '∀' umgewandelt.
 root.absRuleLet=Abs-Regel mit Let
 root.varRuleLet=Var-Regel mit Let
 root.selectLanguage=Sprache
 root.termExplanation=Die folgende Grammatik beschreibt den Aufbau eines gültigen Terms:
-root.assExplanation=Die folgende Grammatik beschreibt die Syntax eines gültigen Typs:
+root.assExplanation=Im Typannahmen-Eingabefeld werden einzelne Typannahmen durch ein Semikolon \
+(<span style="font-family: Arial Black">;</span>)<br>voneinander getrennt. Variable und Typ einer Typannahme werden \
+durch einen<br>Doppelpunkt (<span style="font-family: Arial Black">:</span>) separiert.
+root.typeExplanation=Die folgende Grammatik beschreibt die Syntax eines gültigen Typs:
 root.typeAssumptions=Typannahmen
 root.typeAssumptionsHint=Um die Typannahmen auf den Term anzuwenden, muss neu typisiert werden.
 root.addAssumption=Typannahme hinzufügen
@@ -48,9 +52,9 @@ root.helpInputField=In das Eingabefeld können Lambda-Terme mit einer Länge von
 Das λ-Zeichen kann dabei entweder durch Klicken des λ-Knopfs oder durch Eingabe eines Backslashs \
 eingefügt werden. Durch Klicken des Info-Symbols wird die korrekte Syntax eines Terms \
 angezeigt.
-root.helpTypeAssumptions=Durch Klicken des Typannahmen-Knopfs öffnet sich ein Dialog zur Eingabe von Typannahmen. \
+root.helpTypeAssumptions=In das Typannahmen-Eingabefeld kann eine beliebige Anzahl an Typannahmen eingegeben werden. \
-Durch Klicken des Info-Symbols wird die korrekte Syntax des Typs einer Typannahme angezeigt. Sofern eine Variable in \
+Durch Klicken des Info-Symbols wird die korrekte Syntax der Typannahmen angezeigt. Sofern eine Variable in \
-mehreren Typannahmen vorkommt, wird ausschließlich die oberste Typannahme, die diese Variable enthält, \
+mehreren Typannahmen vorkommt, wird ausschließlich die erste Typannahme, die diese Variable enthält, \
 berücksichtigt. Falls der Typ einer Typannahme mit einem 't' beginnt und anschließend nur Ziffern folgen, wird der Typ \
 automatisch zu einer Typvariable.
 root.helpTypeInferButton=Durch Benutzen des Typisieren-Knopfs wird die Berechnung des Typinferenzalgorithmus mit \

src/main/resources/language/translation_en.properties

@@ -16,9 +16,13 @@ root.letRule=Let rule
 root.absRuleLet=Abs rule with Let
 root.varRuleLet=Var rule with Let
 root.inputFieldPlaceholder=Enter term here. A '\\' is converted to '\u03BB'.
+root.typeInputFieldPlaceholder=Enter type assumptions here. A '!' is converted to '∀'.
 root.selectLanguage=Language
 root.termExplanation=The following grammar specifies the structure of a valid term:
-root.assExplanation=The following grammar specifies the syntax of a valid type:
+root.assExplanation=In the type assumption input field, type assumptions are separated by a semicolon \
+(<span style="font-family: Arial Black">;</span>).<br> The variable and type of a type assumption are separated by a colon \
+(<span style="font-family: Arial Black">:</span>).
+root.typeExplanation=The following grammar specifies the syntax of a valid type:
 root.typeAssumptions=Type Assumptions
 root.typeAssumptionsHint=To apply the type assumptions to the current term, you need to press "Type".
 root.addAssumption=Add Type Assumption
@@ -46,9 +50,9 @@ modified.
 root.helpInputField=The input field allows the user to enter lambda terms with a maximum length of 1000 characters. \
 The λ character can be inserted by either clicking the λ button or entering a backslash. \
 By clicking on the info icon the grammar defining the valid input syntax is shown.
-root.helpTypeAssumptions=Clicking on the type assumptions button opens up a dialog to enter type assumptions. \
+root.helpTypeAssumptions=The type assumption input field allows the user to enter any number of type assumptions. \
-By clicking the icon symbol the grammar defining a valid type of a type assumption is shown. If the same variable \
+By clicking the icon symbol the grammar defining valid type assumptions is shown. If the same variable \
-is contained in multiple type assumptions, only the uppermost type assumption containing the variable is used for \
+is contained in multiple type assumptions, only the first type assumption containing the variable is used for \
 the algorithm. If the type of a type assumptions starts with a 't' followed by only digits, the type is automatically \
 converted to a type variable.
 root.helpTypeInferButton=Clicking on the type button starts the type inference algorithm for the current input. \