mark all texts for translation #179

client/i18next-scanner.config.cjs

@@ -99,7 +99,7 @@ module.exports = {
     },
     lngs: ['en','de'],
     ns: [],
-    defaultLng: 'en-GB',
+    defaultLng: 'en',
     defaultNs: 'translation',
     defaultValue: (lng, ns, key) => {
       if (lng === 'en') {
@@ -139,15 +139,9 @@ module.exports = {
       'use strict';
       const parser = this.parser;
 
-      let count = 0;
-
       parser.parseTransFromString(outputText);
       parser.parseFuncFromString(outputText);
 
-        if (count > 0) {
-          console.log(`[i18next-scanner] transform: count=${chalk.cyan(count)}, file=${chalk.yellow(JSON.stringify(file.relative))}`);
-        }
-
       done();
     }
   ),

client/public/locales/de/translation.json

@@ -38,5 +38,54 @@
   "back to games selection": "",
   "close inventory": "",
   "show inventory": "",
-  "World": ""
+  "World": "",
+  "Show more help!": "",
+  "Goal": "",
+  "Current Goal": "",
+  "Objects": "",
+  "Assumptions": "",
+  "Further Goals": "",
+  "No Goals": "",
+  "Loading goal…": "",
+  "Click somewhere in the Lean file to enable the infoview.": "",
+  "Waiting for Lean server to start…": "",
+  "Level completed! 🎉": "",
+  "Level completed with warnings 🎭": "",
+  "Retry proof from here": "",
+  "Active Goal": "",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "",
+  "Line": "",
+  "Character": "",
+  "Loading messages…": "",
+  "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>": "",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "",
+  "<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": "",
+  "Worlds": "",
+  "Levels": "",
+  "Language": "",
+  "Development notes": "",
+  "Adding new games": "",
+  "Funding": "",
+  "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "",
+  "Delete Progress?": "",
+  "Delete": "",
+  "Download & Delete": "",
+  "Cancel": "",
+  "Layout": "",
+  "Always visible": "",
+  "Save my settings (in the browser store)": "",
+  "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "",
+  "Upload Saved Progress": "",
+  "Load selected file": ""
 }

client/public/locales/en/translation.json

@@ -38,5 +38,54 @@
   "back to games selection": "back to games selection",
   "close inventory": "close inventory",
   "show inventory": "show inventory",
-  "World": "World"
+  "World": "World",
+  "Show more help!": "Show more help!",
+  "Goal": "Goal",
+  "Current Goal": "Current Goal",
+  "Objects": "Objects",
+  "Assumptions": "Assumptions",
+  "Further Goals": "Further Goals",
+  "No Goals": "No Goals",
+  "Loading goal…": "Loading goal…",
+  "Click somewhere in the Lean file to enable the infoview.": "Click somewhere in the Lean file to enable the infoview.",
+  "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",
+  "Character": "Character",
+  "Loading messages…": "Loading messages…",
+  "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>",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.",
+  "<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>": "<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>": "<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.": "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": "Prerequisites",
+  "Worlds": "Worlds",
+  "Levels": "Levels",
+  "Language": "Language",
+  "Development notes": "Development notes",
+  "Adding new games": "Adding new games",
+  "Funding": "Funding",
+  "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>",
+  "Delete Progress?": "Delete Progress?",
+  "Delete": "Delete",
+  "Download & Delete": "Download & Delete",
+  "Cancel": "Cancel",
+  "Layout": "Layout",
+  "Always visible": "Always visible",
+  "Save my settings (in the browser store)": "Save my settings (in the browser store)",
+  "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>",
+  "Upload Saved Progress": "Upload Saved Progress",
+  "Load selected file": "Load selected file"
 }

client/src/components/app_bar.tsx

@@ -13,13 +13,14 @@ import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress }
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { Button } from './button'
 import { downloadProgress } from './popup/erase'
-import { t } from 'i18next'
+import { useTranslation } from 'react-i18next'
 
 /** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */
 function MobileNavButtons({pageNumber, setPageNumber}:
   { pageNumber: number,
     setPageNumber: any}) {
   const gameId = React.useContext(GameIdContext)
+  const { t } = useTranslation()
   const dispatch = useAppDispatch()
 
   // if `prevText` or `prevIcon` is set, show a button to go back
@@ -64,6 +65,7 @@ function MenuButton({navOpen, setNavOpen}) {
  * for the last level, this button turns into a button going back to the welcome page.
  */
 function NextButton({worldSize, difficulty, completed, setNavOpen}) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
   return (levelId < worldSize ?
@@ -84,6 +86,7 @@ function NextButton({worldSize, difficulty, completed, setNavOpen}) {
  * only renders if the current level id is > 0.
  */
 function PreviousButton({setNavOpen}) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
   return (levelId > 0 && <>
@@ -98,6 +101,7 @@ function PreviousButton({setNavOpen}) {
 
 /** button to toggle between editor and typewriter */
 function InputModeButton({setNavOpen, isDropdown}) {
+  const { t } = useTranslation()
   const {levelId} = React.useContext(WorldLevelIdContext)
   const {typewriterMode, setTypewriterMode, lockEditorMode} = React.useContext(InputModeContext)
 
@@ -124,6 +128,7 @@ function InputModeButton({setNavOpen, isDropdown}) {
  * Note: Do not translate the word "Impressum"! German GDPR needs this.
 */
 function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
+  const { t } = useTranslation()
   return <Button className="btn btn-inverted"
     title={t("information, Impressum, privacy policy")} inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
     <FontAwesomeIcon icon={faCircleInfo} />
@@ -132,38 +137,44 @@ function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
 }
 
 function PreferencesButton({setNavOpen, togglePreferencesPopup}) {
+  const { t } = useTranslation()
   return <Button title={t("Preferences")} inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
     <FontAwesomeIcon icon={faGear} />&nbsp;{t("Preferences")}
   </Button>
 }
 
 function GameInfoButton({setNavOpen, toggleInfo}) {
+  const { t } = useTranslation()
   return <Button className="btn btn-inverted"
     title={t("Game Info & Credits")} inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
     <FontAwesomeIcon icon={faCircleInfo} />&nbsp;{t("Game Info")}
   </Button>
 }
 
 function EraseButton ({setNavOpen, toggleEraseMenu}) {
+  const { t } = useTranslation()
   return <Button title={t("Clear Progress")} inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
     <FontAwesomeIcon icon={faEraser} />&nbsp;{t("Erase")}
   </Button>
 }
 
 function DownloadButton ({setNavOpen, gameId, gameProgress}) {
+  const { t } = useTranslation()
   return <Button title={t("Download Progress")} inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
     <FontAwesomeIcon icon={faDownload} />&nbsp;{t("Download")}
   </Button>
 }
 
 function UploadButton ({setNavOpen, toggleUploadMenu}) {
+  const { t } = useTranslation()
   return <Button title={t("Load Progress from JSON")} inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
     <FontAwesomeIcon icon={faUpload} />&nbsp;{t("Upload")}
   </Button>
 }
 
 /**  button to go back to welcome page */
 function HomeButton({isDropdown}) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   return <Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
     <FontAwesomeIcon icon={faHome} />
@@ -172,6 +183,7 @@ function HomeButton({isDropdown}) {
 }
 
 function LandingPageButton() {
+  const { t } = useTranslation()
   return <Button inverted="false" title={t("back to games selection")} to="/">
     <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
     </Button>
@@ -181,6 +193,7 @@ function LandingPageButton() {
  * only displays a button if `setPageNumber` is set.
  */
 function InventoryButton({pageNumber, setPageNumber}) {
+  const { t } = useTranslation()
   return (setPageNumber &&
     <Button to="" className="btn btn-inverted toggle-width"
       title={pageNumber ? t("close inventory") : t("show inventory")}
@@ -239,6 +252,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, toggleInfo,
   pageNumber?: number,
   setPageNumber?: any,
 }) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(PreferencesContext)

client/src/components/hints.tsx

@@ -4,6 +4,7 @@ import Markdown from './markdown';
 import { DeletedChatContext, ProofContext } from "./infoview/context";
 import { lastStepHasErrors } from "./infoview/goals";
 import { Button } from "./button";
+import { useTranslation } from "react-i18next";
 
 /** Plug-in the variable names in a hint. We do this client-side to prepare
  * for i18n in the future. i.e. one should be able translate the `rawText`
@@ -88,6 +89,8 @@ function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
 
 export function MoreHelpButton({selected=null} : {selected?: number}) {
 
+  const { t } = useTranslation()
+
   const {proof, setProof} = React.useContext(ProofContext)
   const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
 
@@ -113,7 +116,7 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
 
   if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
     return <Button to="" onClick={activateHiddenHints}>
-      Show more help!
+      {t("Show more help!")}
     </Button>
   }
 }

client/src/components/infoview/goals.tsx

@@ -14,6 +14,7 @@ import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, Interacti
 import { RpcSessionAtPos } from '@leanprover/infoview/*';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { DiagnosticSeverity } from 'vscode-languageserver-protocol';
+import { useTranslation } from 'react-i18next';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -134,11 +135,6 @@ interface GoalProps {
     typewriter: boolean
 }
 
-interface ProofDisplayProps {
-  proof: string
-}
-
-
 /**
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
@@ -186,6 +182,7 @@ export const Goal = React.memo((props: GoalProps) => {
 })
 
 export const MainAssumptions = React.memo((props: GoalProps2) => {
+  let { t } = useTranslation()
   const { goals, filter } = props
 
   const goal = goals[0]
@@ -200,7 +197,7 @@ export const MainAssumptions = React.memo((props: GoalProps2) => {
       [locs, goal.mvarId])
 
   const goalLi = <div key={'goal'}>
-    <div className="goal-title">Goal: </div>
+    <div className="goal-title">{t("Goal") + ":"}</div>
     <LocationsContext.Provider value={goalLocs}>
       <InteractiveCode fmt={goal.type} />
     </LocationsContext.Provider>
@@ -210,25 +207,26 @@ export const MainAssumptions = React.memo((props: GoalProps2) => {
   const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
 
   return <div id="main-assumptions">
-    <div className="goals-section-title">Current Goal</div>
+    <div className="goals-section-title">{t("Current Goal")}</div>
     {filter.reverse && goalLi}
     { objectHyps.length > 0 &&
-      <div className="hyp-group"><div className="hyp-group-title">Objects:</div>
+      <div className="hyp-group"><div className="hyp-group-title">{t("Objects") + ":"}</div>
       {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
     { assumptionHyps.length > 0 &&
       <div className="hyp-group">
-        <div className="hyp-group-title">Assumptions:</div>
+        <div className="hyp-group-title">{t("Assumptions") + ":"}</div>
         {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
       </div> }
   </div>
 })
 
 export const OtherGoals = React.memo((props: GoalProps2) => {
+  let { t } = useTranslation()
   const { goals, filter } = props
   return <>
     {goals && goals.length > 1 &&
       <div id="other-goals" className="other-goals">
-        <div className="goals-section-title">Further Goals</div>
+        <div className="goals-section-title">{t("Further Goals")}</div>
         {goals.slice(1).map((goal, i) =>
           <details key={i}>
             <summary>
@@ -240,25 +238,6 @@ export const OtherGoals = React.memo((props: GoalProps2) => {
   </>
 })
 
-// TODO: deprecated
-export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
-  const { proof } = props
-  const steps = proof.match(/.+/g)
-  return <>
-    { steps &&
-      <div id="current-proof">
-        <div className="goals-section-title">Proof history</div>
-        <div className="proof-display-wrapper">
-          <div className="proof-display">
-            {steps.map((s) =>
-              <div>{s}</div>
-            )}
-          </div>
-        </div>
-      </div>}
-  </>
-})
-
 interface GoalsProps {
     goals: InteractiveGoalsWithHints
     filter: GoalFilterState