more progress on internationalisation

pull/205/head
Jon Eugster 2 years ago
parent 7e9514fe96
commit ebda6cc162

@ -1,6 +1,6 @@
{ {
"Tactics": "Taktiken", "Tactics": "Taktiken",
"Lean Game Server": "Lean-Spieleserver", "Lean Game Server": "Lean-Spielserver",
"<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>": "<p>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwending sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.", "<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>": "<p>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwending sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.",
"Game Rules": "Spielregeln", "Game Rules": "Spielregeln",
"levels": "Levels", "levels": "Levels",
@ -24,8 +24,7 @@
"Editor mode": "", "Editor mode": "",
"Typewriter mode": "", "Typewriter mode": "",
"information, Impressum, privacy policy": "", "information, Impressum, privacy policy": "",
"Impressum": "", "Preferences": "Einstellungen",
"Preferences": "",
"Game Info & Credits": "", "Game Info & Credits": "",
"Game Info": "", "Game Info": "",
"Clear Progress": "", "Clear Progress": "",
@ -65,15 +64,15 @@
"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>": "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.": "", "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": "Voraussetzungen",
"Worlds": "", "Worlds": "Welten",
"Levels": "", "Levels": "Levels",
"Language": "", "Language": "Sprachen",
"Development notes": "", "Development notes": "",
"Adding new games": "", "Adding new games": "",
"Funding": "", "Funding": "",
@ -82,9 +81,9 @@
"Delete": "", "Delete": "",
"Download & Delete": "", "Download & Delete": "",
"Cancel": "", "Cancel": "",
"Layout": "", "Layout": "Seitenlayout",
"Always visible": "", "Always visible": "",
"Save my settings (in the browser store)": "", "Save my settings (in the browser store)": "Einstellungen im Browser speichern.",
"<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": ""

@ -55,7 +55,7 @@ function MobileNavButtons({pageNumber, setPageNumber}:
} }
/** button to toggle dropdown menu. */ /** button to toggle dropdown menu. */
function MenuButton({navOpen, setNavOpen}) { export function MenuButton({navOpen, setNavOpen}) {
return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}> return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}>
{navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />} {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
</Button> </Button>
@ -127,16 +127,16 @@ function InputModeButton({setNavOpen, isDropdown}) {
* *
* Note: Do not translate the word "Impressum"! German GDPR needs this. * Note: Do not translate the word "Impressum"! German GDPR needs this.
*/ */
function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) { export function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
const { t } = useTranslation() const { t } = useTranslation()
return <Button className="btn btn-inverted" return <Button className="btn btn-inverted"
title={t("information, Impressum, privacy policy")} inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}> title={t("information, Impressum, privacy policy")} inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
<FontAwesomeIcon icon={faCircleInfo} /> <FontAwesomeIcon icon={faCircleInfo} />
{isDropdown && <>&nbsp;{t("Impressum")}</>} {isDropdown && <>&nbsp;Impressum</>}
</Button> </Button>
} }
function PreferencesButton({setNavOpen, togglePreferencesPopup}) { export function PreferencesButton({setNavOpen, togglePreferencesPopup}) {
const { t } = useTranslation() const { t } = useTranslation()
return <Button title={t("Preferences")} inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}> return <Button title={t("Preferences")} inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
<FontAwesomeIcon icon={faGear} />&nbsp;{t("Preferences")} <FontAwesomeIcon icon={faGear} />&nbsp;{t("Preferences")}

@ -16,6 +16,8 @@ import { GameTile, useGetGameInfoQuery } from '../state/api'
import path from 'path'; import path from 'path';
import lean4gameConfig from '../config.json' import lean4gameConfig from '../config.json'
import { PreferencesPopup } from './popup/preferences';
import { ImpressumButton, MenuButton, PreferencesButton } from './app_bar';
const flag = { const flag = {
'Dutch': '🇳🇱', 'Dutch': '🇳🇱',
@ -84,24 +86,28 @@ function LandingPage() {
const navigate = useNavigate(); const navigate = useNavigate();
const [impressum, setImpressum] = React.useState(false); const [impressumPopup, setImpressumPopup] = React.useState(false);
const openImpressum = () => setImpressum(true); const [preferencesPopup, setPreferencesPopup] = React.useState(false);
const closeImpressum = () => setImpressum(false); const [navOpen, setNavOpen] = React.useState(false);
const openImpressum = () => setImpressumPopup(true);
const closeImpressum = () => setImpressumPopup(false);
const toggleImpressum = () => setImpressumPopup(!impressumPopup);
const closePreferencesPopup = () => setPreferencesPopup(false);
const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup);
let allTiles = lean4gameConfig.allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) let allTiles = lean4gameConfig.allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
const { t, i18n } = useTranslation() const { t, i18n } = useTranslation()
return <div className="landing-page"> return <div className="landing-page">
<header style={{backgroundImage: `url(${bgImage})`}}> <header style={{backgroundImage: `url(${bgImage})`}}>
<nav> <nav className="landing-page-nav">
<GithubIcon url="https://github.com/leanprover-community/lean4game"/> <GithubIcon url="https://github.com/leanprover-community/lean4game"/>
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
</div>
</nav> </nav>
<div>
<button onClick={() => i18n.changeLanguage("en")}>{flag["English"]}</button>
<button onClick={() => i18n.changeLanguage("fr")}>{flag["French"]}</button>
<button onClick={() => i18n.changeLanguage("de")}>{flag["German"]}</button>
{/* Add more buttons for other languages as needed */}
</div>
<div id="main-title"> <div id="main-title">
<h1>{t("Lean Game Server")}</h1> <h1>{t("Lean Game Server")}</h1>
<p> <p>
@ -185,7 +191,8 @@ function LandingPage() {
<footer> <footer>
{/* Do not translate "Impressum", it's needed for German GDPR */} {/* Do not translate "Impressum", it's needed for German GDPR */}
<a className="link" onClick={openImpressum}>Impressum</a> <a className="link" onClick={openImpressum}>Impressum</a>
{impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null} {impressumPopup? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
{preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
</footer> </footer>
</div> </div>

@ -62,7 +62,6 @@ function Level() {
const levelId = parseInt(params.levelId) const levelId = parseInt(params.levelId)
const worldId = params.worldId const worldId = params.worldId
const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
const gameId = React.useContext(GameIdContext) const gameId = React.useContext(GameIdContext)
const gameInfo = useGetGameInfoQuery({game: gameId}) const gameInfo = useGetGameInfoQuery({game: gameId})
@ -84,7 +83,7 @@ function Level() {
<PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>} <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>}
{impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null} {impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
{info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null} {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
{preferencesPopup ? <PreferencesPopup layout={layout} isSavePreferences={isSavePreferences} setLayout={setLayout} setIsSavePreferences={setIsSavePreferences} handleClose={closePreferencesPopup} language={language} setLanguage={setLanguage}/> : null} {preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
</WorldLevelIdContext.Provider> </WorldLevelIdContext.Provider>
} }

@ -8,31 +8,28 @@ import lean4gameConfig from '../../config.json'
import FormControlLabel from '@mui/material/FormControlLabel'; import FormControlLabel from '@mui/material/FormControlLabel';
import { IPreferencesContext } from "../infoview/context" import { IPreferencesContext, PreferencesContext } from "../infoview/context"
import ReactCountryFlag from 'react-country-flag'; import ReactCountryFlag from 'react-country-flag';
import { useTranslation } from 'react-i18next'; import { useTranslation } from 'react-i18next';
interface PreferencesPopupProps extends Omit<IPreferencesContext, 'mobile'> { export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
handleClose: () => void
}
export function PreferencesPopup({ layout, setLayout, isSavePreferences, language, setIsSavePreferences, handleClose, setLanguage }: PreferencesPopupProps) {
let { t } = useTranslation() let { t } = useTranslation()
const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
const marks = [ const marks = [
{ {
value: 0, value: 0,
label: 'Mobile', label: t('Mobile'),
key: "mobile" key: "mobile"
}, },
{ {
value: 1, value: 1,
label: 'Auto', label: t('Auto'),
key: "auto" key: "auto"
}, },
{ {
value: 2, value: 2,
label: 'Desktop', label: t('Desktop'),
key: "desktop" key: "desktop"
}, },
]; ];

@ -135,7 +135,7 @@ function Welcome() {
{eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null} {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
{uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null} {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
{info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null} {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
{preferencesPopup ? <PreferencesPopup layout={layout} isSavePreferences={isSavePreferences} setLayout={setLayout} setIsSavePreferences={setIsSavePreferences} handleClose={closePreferencesPopup} language={language} setLanguage={setLanguage}/> : null} {preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
</> </>
} }

@ -36,6 +36,13 @@ a {
padding-bottom: 80px; padding-bottom: 80px;
} }
.landing-page-nav {
position: relative;
}
#menu-btn {
background-color: unset;
}
@media screen and (max-width: 440px) { @media screen and (max-width: 440px) {
.game-list { .game-list {

@ -21,7 +21,14 @@ let root_object: RouteObject = single_game ? {
loader: () => redirect("/g/local/game") loader: () => redirect("/g/local/game")
} : { } : {
path: "/", path: "/",
element: <LandingPage />, element: <App />,
errorElement: <ErrorPage />,
children: [
{
path: "/",
element: <LandingPage />,
}
]
} }
const router = createHashRouter([ const router = createHashRouter([

Loading…
Cancel
Save