From 99c0e8332db545eb6fd748f3d69c9b76bd166c6e Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Tue, 22 Jun 2021 15:29:18 +0200 Subject: [PATCH] Update InfoDialog and HelpDialog --- .../edu/kit/typicalc/view/main/InfoContent.java | 15 +++++++++------ .../java/edu/kit/typicalc/view/main/InputBar.java | 2 +- src/main/resources/language/general.properties | 6 ++++-- .../resources/language/translation_de.properties | 12 ++++++++---- .../resources/language/translation_en.properties | 12 ++++++++---- 5 files changed, 30 insertions(+), 17 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/main/InfoContent.java b/src/main/java/edu/kit/typicalc/view/main/InfoContent.java index 0568a35..636d7eb 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InfoContent.java +++ b/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); - add(termExplanation, termSyntax, assExplanation, assSyntax); + typeSyntax.setId(GRAMMAR_ID); + 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")); - assSyntax.getElement().setProperty("innerHTML", getTranslation("root.assGrammar")); + assExplanation.getElement().setProperty("innerHTML", getTranslation("root.assExplanation")); + typeExplanation.setText(getTranslation("root.typeExplanation")); + typeSyntax.getElement().setProperty("innerHTML", getTranslation("root.typeGrammar")); } } diff --git a/src/main/java/edu/kit/typicalc/view/main/InputBar.java b/src/main/java/edu/kit/typicalc/view/main/InputBar.java index 99564c4..84aeae8 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/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")); } } diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties index 83b94d0..35cfc6b 100644 --- a/src/main/resources/language/general.properties +++ b/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]*
\ \u2329Const\u232A ::= [0-9]+ | true | false -root.assGrammar=\u2329Type\u232A ::= (\u2329Type\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \ +root.typeGrammar=\u2329Type\u232A ::= \u2329QuantifiedType\u232A | \u2329NormalType\u232A
\ +\u2329QuantifiedType\u232A ::= ∀\u2329VarType\u232A.\u2329NormalType\u232A
\ +\u2329NormalType\u232A ::= (\u2329NormalType\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \ \u2329FunctionType\u232A
\ \u2329NamedType\u232A ::= [a-zA-Z][a-zA-Z0-9]*  \\t[0-9]+
\ \u2329VarType\u232A ::= t[0-9]+
\ -\u2329FunctionType\u232A ::= \u2329Type\u232A -> \u2329Type\u232A +\u2329FunctionType\u232A ::= \u2329NormalType\u232A -> \u2329NormalType\u232A root.appLatex=\ \\begin{prooftree}\ diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index 2b0e2c6..16f8e8c 100644 --- a/src/main/resources/language/translation_de.properties +++ b/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 \ +(;)
voneinander getrennt. Variable und Typ einer Typannahme werden \ +durch einen
Doppelpunkt (:) 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. \ -Durch Klicken des Info-Symbols wird die korrekte Syntax des Typs einer Typannahme angezeigt. Sofern eine Variable in \ -mehreren Typannahmen vorkommt, wird ausschließlich die oberste Typannahme, die diese Variable enthält, \ +root.helpTypeAssumptions=In das Typannahmen-Eingabefeld kann eine beliebige Anzahl an Typannahmen eingegeben werden. \ +Durch Klicken des Info-Symbols wird die korrekte Syntax der Typannahmen angezeigt. Sofern eine Variable in \ +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 \ diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties index f56601f..34e853a 100644 --- a/src/main/resources/language/translation_en.properties +++ b/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 \ +(;).
The variable and type of a type assumption are separated by a colon \ +(:). +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. \ -By clicking the icon symbol the grammar defining a valid type of a type assumption is shown. If the same variable \ -is contained in multiple type assumptions, only the uppermost type assumption containing the variable is used for \ +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 valid type assumptions is shown. If the same variable \ +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. \