diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index c522536..26ab89b 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -19,6 +19,7 @@ import { PreferencesPopup } from './popup/preferences'; import { ImpressumButton, MenuButton, PreferencesButton } from './app_bar'; import ReactCountryFlag from 'react-country-flag'; import lean4gameConfig from '../config.json' +import i18next from 'i18next'; function GithubIcon({url='https://github.com'}) { @@ -32,7 +33,7 @@ function GithubIcon({url='https://github.com'}) { } function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { - let { t } = useTranslation() + let { t, i18n } = useTranslation() let navigate = useNavigate(); const routeChange = () =>{ navigate(gameId); @@ -42,19 +43,22 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { return <> } + // Load the namespace of the game + i18next.loadNamespaces(gameId) + return
-
{data.title}
-
{data.short} +
{t(data.title, { ns: gameId })}
+
{t(data.short, { ns: gameId })}
{ data.image ? :
} -
{data.long}
+
{t(data.long, { ns: gameId })}
- + diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 1c5b1b9..b0582d4 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -53,6 +53,8 @@ import { onigasmH } from 'onigasm/lib/onigasmH' import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals' import { InfoPopup } from './popup/game_info' import { PreferencesPopup } from './popup/preferences' +import { useTranslation } from 'react-i18next' +import i18next from 'i18next' monacoSetup() @@ -63,6 +65,10 @@ function Level() { const worldId = params.worldId const gameId = React.useContext(GameIdContext) + + // Load the namespace of the game + i18next.loadNamespaces(gameId) + const gameInfo = useGetGameInfoQuery({game: gameId}) // pop-ups @@ -88,6 +94,7 @@ function Level() { } function ChatPanel({lastLevel, visible = true}) { + let { t } = useTranslation() const chatRef = useRef(null) const {mobile} = useContext(PreferencesContext) const gameId = useContext(GameIdContext) @@ -134,7 +141,7 @@ function ChatPanel({lastLevel, visible = true}) { // // chatRef.current!.scrollTo(0,0) // }, [gameId, worldId, levelId]) - let introText: Array = level?.data?.introduction.split(/\n(\s*\n)+/) + let introText: Array = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/) return
@@ -441,11 +448,12 @@ function PlayableLevel({impressum, setImpressum, toggleInfo, togglePreferencesPo } function IntroductionPanel({gameInfo}) { + let { t } = useTranslation() const gameId = React.useContext(GameIdContext) const {worldId} = useContext(WorldLevelIdContext) const {mobile} = React.useContext(PreferencesContext) - let text: Array = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/) + let text: Array = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/) return
diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index 676e278..ecc1c74 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -23,19 +23,24 @@ import { WorldTreePanel } from './world_tree' import '../css/welcome.css' import { WelcomeAppBar } from './app_bar' import { Hint } from './hints' +import i18next from 'i18next' +import { useTranslation } from 'react-i18next' /** the panel showing the game's introduction text */ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) { const {mobile} = React.useContext(PreferencesContext) const gameId = React.useContext(GameIdContext) + + let { t } = useTranslation() + const dispatch = useAppDispatch() // TODO: I left the setup for splitting up the introduction in place, but if it's not needed // then this can be simplified. // let text: Array = introduction.split(/\n(\s*\n)+/) - let text: Array = introduction ? [introduction] : [] + let text: Array = introduction ? [t(introduction, {ns : gameId})] : [] return
@@ -64,6 +69,10 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, /** main page of the game showing among others the tree of worlds/levels */ function Welcome() { const gameId = React.useContext(GameIdContext) + + // Load the namespace of the game + i18next.loadNamespaces(gameId) + const {mobile} = React.useContext(PreferencesContext) const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext) diff --git a/client/src/i18n.ts b/client/src/i18n.ts index 10e25b1..da02ff5 100644 --- a/client/src/i18n.ts +++ b/client/src/i18n.ts @@ -6,6 +6,19 @@ i18n .use(initReactI18next) // passes i18n down to react-i18next .use(Backend) .init({ + ns: ['translation'], + backend: { + // see https://github.com/i18next/i18next-http-backend + + loadPath: function(lngs, namespaces: Array) { + console.warn(namespaces) + if (namespaces[0].startsWith("g/")) { + return '/i18n/{{ns}}/{{lng}}/Game.json'; + } else { + return '/locales/{{lng}}/{{ns}}.json'; + } + } + }, lng: "en", // language to use, more information here: https://www.i18next.com/overview/configuration-options#languages-namespaces-resources // you can use the i18n.changeLanguage function to change the language manually: https://www.i18next.com/overview/api#changelanguage // if you're using a language detector, do not define the lng option diff --git a/relay/index.mjs b/relay/index.mjs index 8d1e9cf..68bd5d4 100644 --- a/relay/index.mjs +++ b/relay/index.mjs @@ -37,6 +37,14 @@ router.get('/import/trigger/:owner/:repo', importTrigger) const server = app .use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game + .use('/i18n/g/:owner/:repo/:lang/*', (req, res, next) => { + const owner = req.params.owner; + const repo = req.params.repo + const lang = req.params.lang + const filename = req.params[0]; + req.url = filename; + express.static(path.join(getGameDir(owner,repo),".i18n",lang))(req, res, next); + }) .use('/data/g/:owner/:repo/*', (req, res, next) => { const owner = req.params.owner; const repo = req.params.repo diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 4b2eb01..0a012f3 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -331,6 +331,9 @@ structure GameParams where diagnostics : GameDiagnostics deriving ToJson, FromJson +-- `snap` and `initParams` are unused +set_option linter.unusedVariables false in + /-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) : IO Unit := do diff --git a/server/GameServer/Helpers/PrettyPrinter.lean b/server/GameServer/Helpers/PrettyPrinter.lean index ae0b7cd..8109565 100644 --- a/server/GameServer/Helpers/PrettyPrinter.lean +++ b/server/GameServer/Helpers/PrettyPrinter.lean @@ -14,9 +14,6 @@ open Lean.Parser Term open PrettyPrinter Delaborator SubExpr open TSyntax.Compat - -#check Command.declSig - open private shouldGroupWithNext evalSyntaxConstant from Lean.PrettyPrinter.Delaborator.Builtins -- def typeSpec := leading_parser " :\\n: " >> termParser diff --git a/server/GameServer/SaveData.lean b/server/GameServer/SaveData.lean index 59443e0..c58cf26 100644 --- a/server/GameServer/SaveData.lean +++ b/server/GameServer/SaveData.lean @@ -59,8 +59,8 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory)) - -- write PO file for translation - I18n.createPOTemplate + -- write file for translation + I18n.createTemplate open GameData diff --git a/server/GameServer/Tactic/LetIntros.lean b/server/GameServer/Tactic/LetIntros.lean index 43b7327..473e0b7 100644 --- a/server/GameServer/Tactic/LetIntros.lean +++ b/server/GameServer/Tactic/LetIntros.lean @@ -52,8 +52,6 @@ If names are provided, it will introduce as many `let` statements as there are n syntax (name := letIntros) "let_intros" : tactic -- (ppSpace colGt (ident <|> hole))* -#check letIntros - @[tactic letIntros] def evalLetIntros : Tactic := fun stx => do match stx with | `(tactic| let_intros) => liftMetaTactic fun mvarId => do diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 63b1501..d34af4f 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/hhu-adam/lean-i18n.git", "type": "git", "subDir": null, - "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5", + "rev": "59fea5bbc2ea22c2ee77ea6a65b0212ac241a56f", "name": "i18n", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}], "name": "GameServer", diff --git a/server/lakefile.lean b/server/lakefile.lean index 4a96578..2fd0de9 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -8,7 +8,7 @@ package GameServer def leanVersion := "v4.6.0" -- TODO require std from git "https://github.com/leanprover/std4.git" @ leanVersion -require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion +require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ "main" -- leanVersion lean_lib GameServer diff --git a/vite.config.ts b/vite.config.ts index 9bc8d40..42d7ab7 100644 --- a/vite.config.ts +++ b/vite.config.ts @@ -44,6 +44,9 @@ export default defineConfig({ '/data': { target: 'http://localhost:8080', }, + '/i18n': { + target: 'http://localhost:8080', + }, } }, resolve: {
{t("Prerequisites")}{data.prerequisites.join(', ')}{t(data.prerequisites.join(', '), { ns: gameId })}
{t("Worlds")}