English version of help content

src/main/resources/language/translation_de.properties

@@ -43,14 +43,15 @@ aktuellen Cursorposition eingefügt werden. Durch Klicken des Info-Symbols wird
 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 die ausschließlich die oberste Typannahme berücksichtigt.
+mehreren Typannahmen vorkommt, wird ausschließlich die oberste Typannahme, die diese Variable enthält, \
+berücksichtigt.
 root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funtion des Knopfs. \
 Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Klicken des Knopfs zurück zum ersten Schritt des \
 Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Klicken des Knopfs \
 in den letzten Schritt des Baums. Der Knopf lässt sich außerdem durch die Tastenkombination "STRG + Linke Pfeiltaste" \
 ansprechen.
 root.helpPreviousStepButton=Durch Klicken des Vorheriger-Schritt Knopfs wird der vorherige Schritt des Algorithmus \
-angezeigt. Der Knopf lässt sich außerdem auf der Tastatur durch die Taste  "Line Pfeiltaste" ansprechen.
+angezeigt. Der Knopf lässt sich außerdem auf der Tastatur durch die Taste  "Linke Pfeiltaste" ansprechen.
 root.helpNextStepButton=Durch Klicken des Nächster-Schritt Knopfs wird der nächste Schritt des Algorithmus angezeigt. \
 Der Knopf lässt sich außerdem durch auf der Tastatur durch die Taste "Rechte Pfeiltaste" ansprechen.
 root.helpLastStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funtion des Knopfs. \
@@ -58,9 +59,10 @@ Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Klicken des Knopf
 Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Klicken des Knopfs \
 vor zur Anzeige des finalen Typs. Der Knopf lässt sich außerdem durch die Tastenkombination \
 "STRG + Rechte Pfeiltaste" ansprechen.
-root.helpShareButton=Durch Klicken des Teilen Knopfs öffnet sich ein Fenster, in dem der LaTeX-Code des finalen \
-Typherleitungsbaums des eingegebenen Terms und die zum einbinden nötigen Pakete angezeigt werden. Zusätzlich dazu \
-wird ein Permalink zur aktuellen Seite, der sowohl den Term als auch die Typannahmen kodiert, angezeigt.
+root.helpShareButton=Durch Klicken des Teilen Knopfs öffnet sich ein Dialog, in dem der LaTeX-Code des finalen \
+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 \
+kodiert.
 
 root.absLetLatex=\
 \\begin{prooftree}\

src/main/resources/language/translation_en.properties

@@ -32,7 +32,34 @@ root.firstStepButton=First Step Button
 root.previousStepButton=Previous Step Button
 root.nextStepButton=Next Step Button
 root.lastStepButton=Last Step Button
-
+root.shareButton=Share Button
+root.helpDrawer=Clicking on the button opens up the drawer. The drawer contains a collection of all type inference \
+rules. By clicking on the copy-button the LaTeX-code of the corresponding rule is copied to the clipboard.
+root.helpExample=Clicking on the button opens up the example dialog. After clicking on an example the corresponding \
+term is inserted into the input field. Now either the type inference algorithm can be started or the term can be \
+modified.
+root.helpInputField=The input field allows the user to enter lambda terms with a maximum length of 1000 characters. \
+The \u03BB-sign can be inserted at the current cursor position by either clicking the \u03BB-button or entering a \
+backslash. By clicking on the info-symbol the grammar defining the valid input synatx is shown.
+root.helpTypeAssumptions=Clicking on the type-assumptions-button opens up a dialog to enter type assumptions. \
+By clicking the info-symbol the grammar defining a valid type of a type assmuption is shown. If the same variable \
+is contained in multiple type assumptions, only the uppermost type assumption containing the variable is used for \
+the algorithm.
+root.helpFirstStepButton=The function of the button depends on the current state of the algorithm execution. \
+If the tree is currently 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 \
+tree. The key combination "CTRL + left arrow key" also executes a click on the button.
+root.helpPreviousStepButton=By clicking the previous-step button the previous step of the algorithm is shown. \
+The key combination "left arrow key" also executes a click on the button.
+root.helpNextStepButton=By clicking the next-step button the next step of the algorithm is shown. \
+The key combination "right arrow key" also executes a click on the button.
+root.helpLastStepButton=The function of the button depends on the current state of the algorithm execution. \
+If the tree is currently built up, clicking on the button shows the last step of the inference tree. \
+If the unification algorithm is already in progress, clicking on the button shows the final type of the  \
+entered term. The key combination "CTRL + right arrow key" also executes a click on the button.
+root.helpShareButton=Clicking the share button opens up a dialog containing the LaTeX-code of the final inference \
+tree and the packages needed to execute the LaTeX-code. In addition a permalink to the current page is provided. \
+This link encodes the current term as well as the current type assumptions.
 
 root.absLetLatex=\
 \\begin{prooftree}\