add some translation keys

client/i18next-scanner.config.cjs

@@ -78,6 +78,7 @@ module.exports = {
   ],
   options: {
     debug: true,
+    removeUnusedKeys: true,
     func: {
       list: ['i18next.t', 'i18n.t', 't'],
       extensions: ['.js', '.jsx'] // not .ts or .tsx since we use i18next-scanner-typescript!

client/public/locales/de/translation.json

@@ -50,7 +50,6 @@
   "Waiting for Lean server to start…": "Warte auf das Starten des Lean-Servers…",
   "Level completed! 🎉": "Level gelöst! 🎉",
   "Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭",
-  "Retry proof from here": "Von hier erneut probieren",
   "Active Goal": "Aktuelles Goal",
   "Crashed! Go to editor mode and fix your proof! Last server response:": "",
   "Line": "Zeile",
@@ -59,15 +58,11 @@
   "Execute": "Ausführen",
   "Definitions": "Definitionen",
   "Theorems": "Theoreme",
-  "locked": "nicht verfügbar",
-  "disabled": "gesperrt",
-  "new": "neu",
   "Not unlocked yet": "Noch nicht verfügbar",
   "Not available in this level": "In diesem Level nicht verfügbar",
   "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean</1> <i>(Lean 4)</i> und dessen mathematische Bibliothek <5>mathlib</5>",
   "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt von einem lokalen Ordner zu laden.",
   "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
-  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we-ll happily add yours.</p>": "",
   "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
   "Prerequisites": "Voraussetzungen",
   "Worlds": "Welten",
@@ -90,5 +85,10 @@
   "Mobile": "Mobil",
   "Auto": "Auto",
   "Desktop": "Desktop",
-  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": ""
+  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
+  "Level": "",
+  "Introduction": "",
+  "Retry proof from here": "",
+  "Retry": "",
+  "Failed command": ""
 }

client/public/locales/en/translation.json

@@ -50,7 +50,6 @@
   "Waiting for Lean server to start…": "Waiting for Lean server to start…",
   "Level completed! 🎉": "Level completed! 🎉",
   "Level completed with warnings 🎭": "Level completed with warnings 🎭",
-  "Retry proof from here": "Retry proof from here",
   "Active Goal": "Active Goal",
   "Crashed! Go to editor mode and fix your proof! Last server response:": "Crashed! Go to editor mode and fix your proof! Last server response:",
   "Line": "Line",
@@ -59,9 +58,6 @@
   "Execute": "Execute",
   "Definitions": "Definitions",
   "Theorems": "Theorems",
-  "locked": "locked",
-  "disabled": "disabled",
-  "new": "new",
   "Not unlocked yet": "Not unlocked yet",
   "Not available in this level": "Not available in this level",
   "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>",
@@ -89,5 +85,10 @@
   "Mobile": "Mobile",
   "Auto": "Auto",
   "Desktop": "Desktop",
-  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>"
+  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>",
+  "Level": "Level",
+  "Introduction": "Introduction",
+  "Retry proof from here": "Retry proof from here",
+  "Retry": "Retry",
+  "Failed command": "Failed command"
 }

client/public/locales/zh/translation.json

@@ -59,9 +59,6 @@
   "Execute": "执行",
   "Definitions": "定义",
   "Theorems": "定理",
-  "locked": "锁定中",
-  "disabled": "已禁用",
-  "new": "新建",
   "Not unlocked yet": "尚未解锁",
   "Not available in this level": "本关卡不提供",
   "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "",
@@ -89,5 +86,9 @@
   "Load selected file": "加载所选文件",
   "Mobile": "移动端",
   "Auto": "自动",
-  "Desktop": "桌面端"
+  "Desktop": "桌面端",
+  "Level": "",
+  "Introduction": "",
+  "Retry": "",
+  "Failed command": ""
 }

client/src/components/infoview/main.tsx

@@ -265,9 +265,10 @@ const goalFilter = {
   showLetValue: true
 }
 
-// TODD: Mark for translation!
 /** The display of a single entered lean command */
 function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) {
+  let {t} = useTranslation()
+
   // The first step will always have an empty command
   if (!proof?.steps[i]?.command) { return <></> }
 
@@ -275,13 +276,13 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
     // If the last step has errors, we display the command in a different style
     // indicating that it will be removed on the next try.
     return <div className="failed-command">
-      <i>Failed command</i>: {proof?.steps[i].command}
+      <i>{t("Failed command")}</i>: {proof?.steps[i].command}
     </div>
   } else {
     return <div className="command">
       <div className="command-text">{proof?.steps[i].command}</div>
-      <Button to="" className="undo-button btn btn-inverted" title={"Retry proof from here"} onClick={deleteProof}>
+      <Button to="" className="undo-button btn btn-inverted" title={t("Retry proof from here")} onClick={deleteProof}>
-        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;{"Retry"}
+        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;{t("Retry")}
       </Button>
     </div>
   }