From 8b5d6ff2f3f8dea00fb912632dc5f2f7d23bb03a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 16 May 2024 23:26:50 +0200 Subject: [PATCH] improve language selection --- client/public/locales/de/translation.json | 2 +- client/public/locales/es/translation.json | 95 +++++++++++++++++++++++ client/src/app.tsx | 16 +++- client/src/components/flag.tsx | 14 ++++ client/src/components/landing_page.tsx | 12 +-- client/src/components/navigation.tsx | 46 +++++++++-- client/src/config.json | 18 ++++- 7 files changed, 183 insertions(+), 20 deletions(-) create mode 100644 client/public/locales/es/translation.json create mode 100644 client/src/components/flag.tsx diff --git a/client/public/locales/de/translation.json b/client/public/locales/de/translation.json index ab851b1..b3018d3 100644 --- a/client/public/locales/de/translation.json +++ b/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", diff --git a/client/public/locales/es/translation.json b/client/public/locales/es/translation.json new file mode 100644 index 0000000..c1283ec --- /dev/null +++ b/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 (Lean 4) and its mathematical library <5>mathlib": "", + "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "", + "

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.

<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "", + "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above 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.

Featured games on this page are added manually. Please get in contact and we'll happily add yours.

": "", + "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics 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": "", + "

Do you want to delete your saved progress irreversibly?

(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)

": "", + "Delete Progress?": "", + "Delete": "", + "Download & Delete": "", + "Cancel": "", + "Mobile": "", + "Auto": "", + "Desktop": "", + "Layout": "", + "Always visible": "", + "Save my settings (in the browser store)": "", + "

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.

<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 in a level, you can use it henceforth in any level.

The options are:

": "", + "Game Rules": "", + "levels": "", + "tactics": "", + "regular": "", + "relaxed": "", + "none": "", + "

Select a JSON file with the saved game progress to load your progress.

<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "", + "Upload Saved Progress": "", + "Load selected file": "", + "Rules": "" +} diff --git a/client/src/app.tsx b/client/src/app.tsx index f4ab3f9..e03786e 100644 --- a/client/src/app.tsx +++ b/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) - }, [language]) + let availableLangs = gameInfo.data?.tile?.languages + 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 (
diff --git a/client/src/components/flag.tsx b/client/src/components/flag.tsx new file mode 100644 index 0000000..540ceac --- /dev/null +++ b/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 + } + return {iso} +} diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 26a08bd..fb6a9f9 100644 --- a/client/src/components/landing_page.tsx +++ b/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}) { {t("Language")} - {data.languages.map((lang) => { - let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang) - if (lean4gameConfig.useFlags) { - return - } else { - return {lang} - } - })} + {data.languages.map((lang) => ( + + ))} diff --git a/client/src/components/navigation.tsx b/client/src/components/navigation.tsx index ce8fa30..3ae7cc1 100644 --- a/client/src/components/navigation.tsx +++ b/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 () {
} + /** 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