improve language selection

client/public/locales/de/translation.json

@@ -9,7 +9,7 @@
   "relaxed": "relaxed",
   "none": "keine",
   "Rules": "Regeln",
-  "Intro": "Inführung",
+  "Intro": "Einführung",
   "Game Introduction": "Spieleinführung",
   "World selection": "Weltenauswahl",
   "Start": "Start",

client/public/locales/es/translation.json

@@ -0,0 +1,95 @@
+{
+  "Intro": "",
+  "Game Introduction": "",
+  "World selection": "",
+  "Start": "",
+  "Inventory": "",
+  "next level": "",
+  "Next": "",
+  "back to world selection": "",
+  "Leave World": "",
+  "previous level": "",
+  "Previous": "",
+  "Editor mode is enforced!": "",
+  "Editor mode": "",
+  "Typewriter mode": "",
+  "information, Impressum, privacy policy": "",
+  "Preferences": "",
+  "Game Info & Credits": "",
+  "Game Info": "",
+  "Clear Progress": "",
+  "Erase": "",
+  "Download Progress": "",
+  "Download": "",
+  "Load Progress from JSON": "",
+  "Upload": "",
+  "Home": "",
+  "back to games selection": "",
+  "close inventory": "",
+  "show inventory": "",
+  "World": "",
+  "Show more help!": "",
+  "Goal": "",
+  "Objects": "",
+  "Assumptions": "",
+  "Current Goal": "",
+  "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 🎭": "",
+  "Failed command": "",
+  "Retry proof from here": "",
+  "Retry": "",
+  "Active Goal": "",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "",
+  "Line": "",
+  "Character": "",
+  "Loading messages…": "",
+  "Execute": "",
+  "Tactics": "",
+  "Definitions": "",
+  "Theorems": "",
+  "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.": "",
+  "view the Lean game server on Github": "",
+  "Prerequisites": "",
+  "Worlds": "",
+  "Levels": "",
+  "Language": "",
+  "Lean Game Server": "",
+  "Development notes": "",
+  "Adding new games": "",
+  "Funding": "",
+  "Level": "",
+  "Introduction": "",
+  "<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": "",
+  "Mobile": "",
+  "Auto": "",
+  "Desktop": "",
+  "Layout": "",
+  "Always visible": "",
+  "Save my settings (in the browser store)": "",
+  "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "",
+  "Game Rules": "",
+  "levels": "",
+  "tactics": "",
+  "regular": "",
+  "relaxed": "",
+  "none": "",
+  "<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": "",
+  "Rules": ""
+}

client/src/app.tsx

@@ -17,6 +17,7 @@ import { useSelector } from 'react-redux';
 import { changeTypewriterMode, selectOpenedIntro, selectTypewriterMode } from './state/progress';
 import { useAppDispatch } from './hooks';
 import { Popup, PopupContext } from './components/popup/popup';
+import { useGetGameInfoQuery } from './state/api';
 
 export const GameIdContext = React.createContext<{
   gameId: string,
@@ -39,6 +40,7 @@ function App() {
   const [typewriterInput, setTypewriterInput] = useState("")
   const [page, setPage] = useState(0)
   const [popupContent, setPopupContent] = useState(null)
+  const gameInfo = useGetGameInfoQuery({game: gameId})
 
 
   const openedIntro = useSelector(selectOpenedIntro(gameId))
@@ -49,10 +51,18 @@ function App() {
     }
   }, [openedIntro])
 
-
   useEffect(() => {
-    i18n.changeLanguage(language)
+    let availableLangs = gameInfo.data?.tile?.languages
-  }, [language])
+    if (gameId && availableLangs?.length > 0 && !(availableLangs.includes(language))) {
+      // if the game is not available in the preferred language, display it in the original
+      // language
+      console.log(`using default language: ${availableLangs[0]}`)
+      i18n.changeLanguage(availableLangs[0])
+    } else {
+      console.log(`using language: ${language}`)
+      i18n.changeLanguage(language)
+    }
+  }, [gameId, gameInfo.data?.tile?.languages, language])
 
   return (
     <div className="app">

client/src/components/flag.tsx

@@ -0,0 +1,14 @@
+import * as React from 'react'
+import ReactCountryFlag from 'react-country-flag'
+import lean4gameConfig from '../config.json'
+
+/** Displays either a flag or the language-code, depending on the settings.
+ * The argument `iso` is an ISO-language code.
+ */
+export const Flag : React.FC<{ iso: string, showTitle?: boolean}> = ({iso, showTitle=false}) => {
+  let lang = lean4gameConfig.newLanguages[iso]
+  if (lean4gameConfig.useFlags && lang) {
+    return <ReactCountryFlag countryCode={lang.flag} title={showTitle ? lang.name : null} />
+  }
+  return <span>{iso}</span>
+}

client/src/components/landing_page.tsx

@@ -19,6 +19,7 @@ import lean4gameConfig from '../config.json'
 import i18next from 'i18next';
 import { useContext } from 'react';
 import { PopupContext } from './popup/popup';
+import { Flag } from './flag';
 
 function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
   let { t } = useTranslation()
@@ -57,14 +58,9 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
         <td>{t("Language")}</td>
 
         <td>
-          {data.languages.map((lang) => {
+          {data.languages.map((lang) => (
-            let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang)
+            <Flag iso={lang} showTitle={true} />
-            if (lean4gameConfig.useFlags) {
+          ))}
-              return <ReactCountryFlag key={`flag-${lang}`} title={langOpt?.name} countryCode={langOpt?.flag} className="emojiFlag"/>
-            } else {
-              return <span key={`flag-text-${lang}`} title={langOpt?.name}>{lang}</span>
-            }
-          })}
         </td>
       </tr>
       </tbody>

client/src/components/navigation.tsx

@@ -1,5 +1,5 @@
 import * as React from 'react'
-import { createContext, useContext, useState } from 'react'
+import { createContext, useContext, useEffect, useState } from 'react'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
   faArrowRight, faArrowLeft, faXmark, faBars, faCode,
@@ -13,6 +13,9 @@ import '../css/navigation.css'
 import { PopupContext } from './popup/popup'
 import { useSelector } from 'react-redux'
 import { selectProgress } from '../state/progress'
+import ReactCountryFlag from 'react-country-flag'
+import lean4gameConfig from '../config.json'
+import { Flag } from './flag'
 
 /** SVG github icon */
 function GithubIcon () {
@@ -208,17 +211,20 @@ function MobileNavigationLevel () {
   </div>
 }
 
+
 /** The skeleton of the navigation which is the same across all layouts. */
 export function Navigation () {
   const { t } = useTranslation()
   const { gameId, worldId } = useContext(GameIdContext)
-  const { mobile } = useContext(PreferencesContext)
+  const { mobile, language, setLanguage } = useContext(PreferencesContext)
   const { setPopupContent } = useContext(PopupContext)
   const gameProgress = useSelector(selectProgress(gameId))
-
+  const gameInfo = useGetGameInfoQuery({game: gameId})
 
   const [navOpen, setNavOpen] = useState(false)
-  function toggleNav () {setNavOpen(!navOpen)}
+  const [langNavOpen, setLangNavOpen] = useState(false)
+  function toggleNav () {setNavOpen(!navOpen); setLangNavOpen(false)}
+  function toggleLangNav () {setLangNavOpen(!langNavOpen); setNavOpen(false)}
 
   return <nav>
     <NavigationContext.Provider value={{navOpen, setNavOpen}}>
@@ -238,13 +244,41 @@ export function Navigation () {
         <NavButton
           iconElement={<GithubIcon />}
           title={t("view the Lean game server on Github")}
-          href='https://github.com/leanprover-community/lean4game'
+          href='https://github.com/leanprover-community/lean4game' />
-        />
+      }
+      {(!gameId || gameInfo.data?.tile?.languages.length > 1) &&
+        // Language button only visible if the game exists in `>1` languages
+        <NavButton
+          iconElement={langNavOpen ? null : <Flag iso={language} />}
+          icon={langNavOpen ? faXmark : null}
+          title={langNavOpen ? t('close language menu') : t('open language menu')}
+          onClick={toggleLangNav}
+          />
       }
       <NavButton
         icon={navOpen ? faXmark : faBars}
         title={navOpen ? t('close menu') : t('open menu')}
         onClick={toggleNav} />
+      { langNavOpen &&
+        <div className='dropdown' onClick={toggleLangNav} >
+          {gameId && gameInfo.data?.tile?.languages ?
+            // Show all languages the game is available in
+            gameInfo.data?.tile?.languages.map(iso =>
+              <NavButton
+                iconElement={<Flag iso={iso} />}
+                text={lean4gameConfig.newLanguages[iso]?.name}
+                onClick={() => {setLanguage(iso)}}
+                inverted={true} />) :
+            // Show all languages the interface is available in (e.g. landing page)
+            Object.entries(lean4gameConfig.newLanguages).map(([iso, val]) =>
+              <NavButton
+                iconElement={<Flag iso={iso} />}
+                text={lean4gameConfig.newLanguages[iso]?.name}
+                onClick={() => {setLanguage(iso)}}
+                inverted={true} />)
+          }
+        </div>
+      }
       { navOpen &&
         <div className='dropdown' onClick={toggleNav} >
           { gameId && <>

client/src/config.json

@@ -1,7 +1,7 @@
 {
   "allGames": [
     "leanprover-community/nng4",
-    "hhu-adam/robo",
+    "local/Robo",
     "djvelleman/stg4",
     "trequetrum/lean4game-logic"
   ],
@@ -23,5 +23,19 @@
       "name": "中文"
     }
   ],
-  "useFlags": false
+  "newLanguages": {
+    "en": {
+      "flag": "GB",
+      "name": "English"
+    },
+    "de": {
+      "flag": "DE",
+      "name": "Deutsch"
+    },
+    "zh": {
+      "flag": "CN",
+      "name": "中文"
+    }
+  },
+  "useFlags": true
 }