implement i18next and i18next-scanner

client/i18next-scanner.config.cjs

@@ -0,0 +1,101 @@
+const typescriptTransform = require('i18next-scanner-typescript');
+
+const fs = require('fs');
+const chalk = require('chalk');
+
+module.exports = {
+    input: [
+        'client/src/**/*.{tsx,ts}',
+        // Use ! to filter out files or directories
+        '!client/i18n/**',
+        '!**/node_modules/**',
+    ],
+    output: './client/public/locales',
+    options: {
+        debug: true,
+        func: {
+            list: ['i18next.t', 'i18n.t', 't'],
+            extensions: ['.js', '.jsx'] // not .ts or .tsx since we use i18next-scanner-typescript!
+        },
+        trans: {
+            component: 'Trans',
+            i18nKey: 'i18nKey',
+            defaultsKey: 'defaults',
+            extensions: ['.js', '.jsx'], // not .ts or .tsx since we use i18next-scanner-typescript!
+            fallbackKey: (ns, value) => {return value},
+
+            // https://react.i18next.com/latest/trans-component#usage-with-simple-html-elements-like-less-than-br-greater-than-and-others-v10.4.0
+            supportBasicHtmlNodes: true, // Enables keeping the name of simple nodes (e.g. <br/>) in translations instead of indexed keys.
+            keepBasicHtmlNodesFor: ['br', 'strong', 'i', 'p'], // Which nodes are allowed to be kept in translations during defaultValue generation of <Trans>.
+
+            // // https://github.com/acornjs/acorn/tree/master/acorn#interface
+            // acorn: {
+            //     ecmaVersion: 2020,
+            //     sourceType: 'module', // defaults to 'module'
+            // }
+        },
+        lngs: ['en','de'],
+        ns: [],
+        defaultLng: 'en',
+        defaultNs: 'translation',
+         defaultValue: (lng, ns, key) => {
+            if (lng === 'en') {
+                return key; // Use key as value for base language
+            }
+            return ''; // Return empty string for other languages
+        },
+        resource: {
+            loadPath: './{{lng}}/{{ns}}.json',
+            savePath: './{{lng}}/{{ns}}.json',
+            jsonIndent: 2,
+            lineEnding: '\n'
+        },
+        nsSeparator: false, // namespace separator
+        keySeparator: false, // key separator
+        plurals: false,
+        interpolation: {
+            prefix: '{{',
+            suffix: '}}'
+        },
+        metadata: {},
+        allowDynamicKeys: false,
+    },
+
+    transform: typescriptTransform(
+        // options
+        {
+          // default value for extensions
+          extensions: [".ts", ".tsx"],
+          // optional ts configuration
+          tsOptions: {
+            target: "es2017",
+          },
+        },
+
+        function(outputText, file, enc, done) {
+            'use strict';
+            const parser = this.parser;
+
+            parser.parseTransFromString(outputText);
+            parser.parseFuncFromString(outputText);
+
+            // const content = fs.readFileSync(file.path, enc);
+            // let count = 0;
+
+            // parser.parseFuncFromString(content, { list: ['i18n._', 'i18n.__'] }, (key, options) => {
+            //     parser.set(key, Object.assign({}, options, {
+            //         nsSeparator: false,
+            //         keySeparator: false
+            //     }));
+            //     ++count;
+            // });
+
+            // 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

@@ -0,0 +1,11 @@
+{
+  "Lean Game Server": "Lean-Spieleserver",
+  "<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",
+  "levels": "Levels",
+  "tactics": "Taktiken",
+  "regular": "regulär",
+  "relaxed": "relaxed",
+  "none": "keine",
+  "Rules": "Regend"
+}

client/public/locales/en/translation.json

@@ -0,0 +1,11 @@
+{
+  "Lean Game Server": "Lean Game Server",
+  "<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>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": "Game Rules",
+  "levels": "levels",
+  "tactics": "tactics",
+  "regular": "regular",
+  "relaxed": "relaxed",
+  "none": "none",
+  "Rules": "Rules"
+}

client/src/components/landing_page.tsx

@@ -139,7 +139,7 @@ function LandingPage() {
     "trequetrum/lean4game-logic",
   ]
   let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
-  const { t, i18n } = useTranslation();
+  const { t, i18n } = useTranslation()
 
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
@@ -149,6 +149,7 @@ function LandingPage() {
       <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">

client/src/components/popup/rules_help.tsx

@@ -2,6 +2,7 @@
  * @fileOverview
 */
 import * as React from 'react'
+import { Trans, useTranslation } from 'react-i18next'
 
 /** Pop-up that is displayed when opening the help explaining the game rules.
  *
@@ -9,11 +10,14 @@ import * as React from 'react'
  * controlled by the containing element.
  */
 export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
+  const { t, i18n } = useTranslation()
+
   return <div className="privacy-policy modal-wrapper">
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Game Rules</h2>
+    <h2>{t("Game Rules")}</h2>
+    <Trans>
       <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.
@@ -24,27 +28,28 @@ export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
         if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
       </p>
       <p>The options are:</p>
+    </Trans>
     <table>
       <thead>
         <tr>
           <th scope="col"></th>
-          <th scope="col">levels</th>
+          <th scope="col">{t("levels")}</th>
-          <th scope="col">tactics</th>
+          <th scope="col">{t("tactics")}</th>
         </tr>
       </thead>
       <tbody>
         <tr>
-          <th scope="row">regular</th>
+          <th scope="row">{t("regular")}</th>
           <td>🔐</td>
           <td>🔐</td>
         </tr>
         <tr>
-          <th scope="row">relaxed</th>
+          <th scope="row">{t("relaxed")}</th>
           <td>🔓</td>
           <td>🔐</td>
         </tr>
         <tr>
-          <th scope="row">none</th>
+          <th scope="row">{t("none")}</th>
           <td>🔓</td>
           <td>🔓</td>
         </tr>

client/src/components/world_tree.tsx

@@ -17,6 +17,7 @@ import { store } from '../state/store'
 
 import '../css/world_tree.css'
 import { PreferencesContext } from './infoview/context'
+import { useTranslation } from 'react-i18next'
 
 // Settings for the world tree
 cytoscape.use( klay )
@@ -195,6 +196,7 @@ export const downloadFile = ({ data, fileName, fileType } :
 
 /** The menu that is shown next to the world selection graph */
 export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
+  const { t, i18n } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
@@ -202,20 +204,20 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
 
 
   function label(x : number) {
-    return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
+    return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular")
   }
 
 
   return <nav className={`world-selection-menu${mobile ? '' : ' desktop'}`}>
     <div className="slider-wrap">
-      <span className="difficulty-label">Rules
+      <span className="difficulty-label">{t("Rules")}
         <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
       </span>
       <Slider
         orientation="vertical"
-        title="Game Rules"
+        title={t("Game Rules")}
         min={0} max={2}
-        aria-label="Game Rules"
+        aria-label={t("Game Rules")}
         value={difficulty}
         marks={[
           {value: 0, label: label(0)},

client/src/i18n.ts

@@ -1,29 +1,11 @@
 import i18n from "i18next";
+import Backend from "i18next-http-backend"
 import { initReactI18next } from "react-i18next";
 
-// the translations
-// (tip move them in a JSON file and import them,
-// or even better, manage them separated from your code: https://react.i18next.com/guides/multiple-translation-files)
-const resources = {
-  en: {
-    translation: {
-      "Welcome to React": "Welcome to React and react-i18next",
-      "Lean Game Server": "Lean Game Server translated"
-
-    }
-  },
-  fr: {
-    translation: {
-      "Welcome to React": "Bienvenue à React et react-i18next",
-      "Lean Game Server": "Lean Game Server French"
-    }
-  }
-};
-
 i18n
 .use(initReactI18next) // passes i18n down to react-i18next
+.use(Backend)
 .init({
-    resources,
     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

package-lock.json

@@ -31,6 +31,8 @@
         "debounce": "^1.2.1",
         "express": "^4.18.2",
         "i18next": "^23.10.1",
+        "i18next-http-backend": "^2.5.0",
+        "i18next-scanner-typescript": "^1.2.0",
         "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
         "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
         "octokit": "^3.1.2",
@@ -64,6 +66,7 @@
         "concurrently": "^7.6.0",
         "css-loader": "^6.7.3",
         "file-loader": "^6.2.0",
+        "i18next-scanner": "^4.4.0",
         "nodemon": "^3.0.1",
         "react-refresh": "^0.14.0",
         "style-loader": "^3.3.1",
@@ -2595,6 +2598,18 @@
         "react": ">=16.3"
       }
     },
+    "node_modules/@gulpjs/to-absolute-glob": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/@gulpjs/to-absolute-glob/-/to-absolute-glob-4.0.0.tgz",
+      "integrity": "sha512-kjotm7XJrJ6v+7knhPaRgaT6q8F8K2jiafwYdNHLzmV0uGLuZY43FK6smNSHUPrhq5kX2slCUy+RGG/xGqmIKA==",
+      "dev": true,
+      "dependencies": {
+        "is-negated-glob": "^1.0.0"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
     "node_modules/@hapi/hoek": {
       "version": "9.3.0",
       "resolved": "https://registry.npmjs.org/@hapi/hoek/-/hoek-9.3.0.tgz",
@@ -5745,6 +5760,21 @@
         "node": ">=0.4.0"
       }
     },
+    "node_modules/acorn-class-fields": {
+      "version": "0.3.7",
+      "resolved": "https://registry.npmjs.org/acorn-class-fields/-/acorn-class-fields-0.3.7.tgz",
+      "integrity": "sha512-jdUWSFce0fuADUljmExz4TWpPkxmRW/ZCPRqeeUzbGf0vFUcpQYbyq52l75qGd0oSwwtAepeL6hgb/naRgvcKQ==",
+      "dev": true,
+      "dependencies": {
+        "acorn-private-class-elements": "^0.2.7"
+      },
+      "engines": {
+        "node": ">=4.8.2"
+      },
+      "peerDependencies": {
+        "acorn": "^6 || ^7 || ^8"
+      }
+    },
     "node_modules/acorn-import-assertions": {
       "version": "1.9.0",
       "resolved": "https://registry.npmjs.org/acorn-import-assertions/-/acorn-import-assertions-1.9.0.tgz",
@@ -5755,6 +5785,83 @@
         "acorn": "^8"
       }
     },
+    "node_modules/acorn-jsx": {
+      "version": "5.3.2",
+      "resolved": "https://registry.npmjs.org/acorn-jsx/-/acorn-jsx-5.3.2.tgz",
+      "integrity": "sha512-rq9s+JNhf0IChjtDXxllJ7g41oZk5SlXtp0LHwyA5cejwn7vKmKp4pPri6YEePv2PU65sAsegbXtIinmDFDXgQ==",
+      "dev": true,
+      "peerDependencies": {
+        "acorn": "^6.0.0 || ^7.0.0 || ^8.0.0"
+      }
+    },
+    "node_modules/acorn-private-class-elements": {
+      "version": "0.2.7",
+      "resolved": "https://registry.npmjs.org/acorn-private-class-elements/-/acorn-private-class-elements-0.2.7.tgz",
+      "integrity": "sha512-+GZH2wOKNZOBI4OOPmzpo4cs6mW297sn6fgIk1dUI08jGjhAaEwvC39mN2gJAg2lmAQJ1rBkFqKWonL3Zz6PVA==",
+      "dev": true,
+      "engines": {
+        "node": ">=4.8.2"
+      },
+      "peerDependencies": {
+        "acorn": "^6.1.0 || ^7 || ^8"
+      }
+    },
+    "node_modules/acorn-private-methods": {
+      "version": "0.3.3",
+      "resolved": "https://registry.npmjs.org/acorn-private-methods/-/acorn-private-methods-0.3.3.tgz",
+      "integrity": "sha512-46oeEol3YFvLSah5m9hGMlNpxDBCEkdceJgf01AjqKYTK9r6HexKs2rgSbLK81pYjZZMonhftuUReGMlbbv05w==",
+      "dev": true,
+      "dependencies": {
+        "acorn-private-class-elements": "^0.2.7"
+      },
+      "engines": {
+        "node": ">=4.8.2"
+      },
+      "peerDependencies": {
+        "acorn": "^6 || ^7 || ^8"
+      }
+    },
+    "node_modules/acorn-stage3": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/acorn-stage3/-/acorn-stage3-4.0.0.tgz",
+      "integrity": "sha512-BR+LaADtA6GTB5prkNqWmlmCLYmkyW0whvSxdHhbupTaro2qBJ95fJDEiRLPUmiACGHPaYyeH9xmNJWdGfXRQw==",
+      "dev": true,
+      "dependencies": {
+        "acorn-class-fields": "^0.3.7",
+        "acorn-private-methods": "^0.3.3",
+        "acorn-static-class-features": "^0.2.4"
+      },
+      "engines": {
+        "node": ">=4.8.2"
+      },
+      "peerDependencies": {
+        "acorn": "^7.4 || ^8"
+      }
+    },
+    "node_modules/acorn-static-class-features": {
+      "version": "0.2.4",
+      "resolved": "https://registry.npmjs.org/acorn-static-class-features/-/acorn-static-class-features-0.2.4.tgz",
+      "integrity": "sha512-5X4mpYq5J3pdndLmIB0+WtFd/mKWnNYpuTlTzj32wUu/PMmEGOiayQ5UrqgwdBNiaZBtDDh5kddpP7Yg2QaQYA==",
+      "dev": true,
+      "dependencies": {
+        "acorn-private-class-elements": "^0.2.7"
+      },
+      "engines": {
+        "node": ">=4.8.2"
+      },
+      "peerDependencies": {
+        "acorn": "^6.1.0 || ^7 || ^8"
+      }
+    },
+    "node_modules/acorn-walk": {
+      "version": "8.3.2",
+      "resolved": "https://registry.npmjs.org/acorn-walk/-/acorn-walk-8.3.2.tgz",
+      "integrity": "sha512-cjkyv4OtNCIeqhHrfS81QWXoCBPExR/J62oyEqepVw8WaQeSqpW2uhuLPh1m9eWhDuOo/jUXVTlifvesOWp/4A==",
+      "dev": true,
+      "engines": {
+        "node": ">=0.4.0"
+      }
+    },
     "node_modules/aggregate-error": {
       "version": "3.1.0",
       "resolved": "https://registry.npmjs.org/aggregate-error/-/aggregate-error-3.1.0.tgz",
@@ -6104,6 +6211,13 @@
       "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz",
       "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw=="
     },
+    "node_modules/bare-events": {
+      "version": "2.2.2",
+      "resolved": "https://registry.npmjs.org/bare-events/-/bare-events-2.2.2.tgz",
+      "integrity": "sha512-h7z00dWdG0PYOQEvChhOSWvOfkIKsdZGkWr083FgN/HyoQuebSew/cgirYqh9SCuy/hRvxc5Vy6Fw8xAmYHLkQ==",
+      "dev": true,
+      "optional": true
+    },
     "node_modules/base64-js": {
       "version": "1.5.1",
       "resolved": "https://registry.npmjs.org/base64-js/-/base64-js-1.5.1.tgz",
@@ -6606,6 +6720,12 @@
         "node": ">=6"
       }
     },
+    "node_modules/clone-stats": {
+      "version": "1.0.0",
+      "resolved": "https://registry.npmjs.org/clone-stats/-/clone-stats-1.0.0.tgz",
+      "integrity": "sha512-au6ydSpg6nsrigcZ4m8Bc9hxjeW+GJ8xh5G3BJCMt4WXe1H10UNaVOamqQTmrx1kjVuxAHIQSNU6hY4Nsn9/ag==",
+      "dev": true
+    },
     "node_modules/clsx": {
       "version": "2.1.0",
       "resolved": "https://registry.npmjs.org/clsx/-/clsx-2.1.0.tgz",
@@ -7007,6 +7127,14 @@
         "yarn": ">=1"
       }
     },
+    "node_modules/cross-fetch": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/cross-fetch/-/cross-fetch-4.0.0.tgz",
+      "integrity": "sha512-e4a5N8lVvuLgAWgnCrLr2PP0YyDOTHa9H/Rj54dirp61qXnNq46m82bRhNqIA5VccJtWBvPTFRV3TtvHUKPB1g==",
+      "dependencies": {
+        "node-fetch": "^2.6.12"
+      }
+    },
     "node_modules/cross-spawn": {
       "version": "7.0.3",
       "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.3.tgz",
@@ -7523,6 +7651,12 @@
         "node": ">=10.13.0"
       }
     },
+    "node_modules/ensure-type": {
+      "version": "1.5.1",
+      "resolved": "https://registry.npmjs.org/ensure-type/-/ensure-type-1.5.1.tgz",
+      "integrity": "sha512-Dxe+mVF4MupV6eueWiFa6hUd9OL9lIM2/LqR40k1P+dwG+G2il2UigXTU9aQlaw+Y/N0BKSaTofNw73htTbC5g==",
+      "dev": true
+    },
     "node_modules/entities": {
       "version": "4.5.0",
       "resolved": "https://registry.npmjs.org/entities/-/entities-4.5.0.tgz",
@@ -7545,6 +7679,12 @@
         "node": ">=4"
       }
     },
+    "node_modules/eol": {
+      "version": "0.9.1",
+      "resolved": "https://registry.npmjs.org/eol/-/eol-0.9.1.tgz",
+      "integrity": "sha512-Ds/TEoZjwggRoz/Q2O7SE3i4Jm66mqTDfmdHdq/7DKVk3bro9Q8h6WdXKdPqFLMoqxrDK5SVRzHVPOS6uuGtrg==",
+      "dev": true
+    },
     "node_modules/error-ex": {
       "version": "1.3.2",
       "resolved": "https://registry.npmjs.org/error-ex/-/error-ex-1.3.2.tgz",
@@ -7699,6 +7839,19 @@
         "node": ">=4"
       }
     },
+    "node_modules/esprima-next": {
+      "version": "5.8.4",
+      "resolved": "https://registry.npmjs.org/esprima-next/-/esprima-next-5.8.4.tgz",
+      "integrity": "sha512-8nYVZ4ioIH4Msjb/XmhnBdz5WRRBaYqevKa1cv9nGJdCehMbzZCPNEEnqfLCZVetUVrUPEcb5IYyu1GG4hFqgg==",
+      "dev": true,
+      "bin": {
+        "esparse": "bin/esparse.js",
+        "esvalidate": "bin/esvalidate.js"
+      },
+      "engines": {
+        "node": ">=12"
+      }
+    },
     "node_modules/esrecurse": {
       "version": "4.3.0",
       "resolved": "https://registry.npmjs.org/esrecurse/-/esrecurse-4.3.0.tgz",
@@ -7866,6 +8019,12 @@
       "resolved": "https://registry.npmjs.org/fast-deep-equal/-/fast-deep-equal-3.1.3.tgz",
       "integrity": "sha512-f3qQ9oQy9j2AhBe/H9VC91wLmKBCCU/gDOnKNAYG5hswO7BLKj09Hc5HYNz9cGI++xlpDCIgDaitVs03ATR84Q=="
     },
+    "node_modules/fast-fifo": {
+      "version": "1.3.2",
+      "resolved": "https://registry.npmjs.org/fast-fifo/-/fast-fifo-1.3.2.tgz",
+      "integrity": "sha512-/d9sfos4yxzpwkDkuN7k2SqFKtYNmCTzgfEpz82x34IM9/zc8KGxQoXg1liNC/izpRM/MBdt44Nmx41ZWqk+FQ==",
+      "dev": true
+    },
     "node_modules/fast-glob": {
       "version": "3.3.2",
       "resolved": "https://registry.npmjs.org/fast-glob/-/fast-glob-3.3.2.tgz",
@@ -8118,6 +8277,19 @@
         "node": ">=6 <7 || >=8"
       }
     },
+    "node_modules/fs-mkdirp-stream": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/fs-mkdirp-stream/-/fs-mkdirp-stream-2.0.1.tgz",
+      "integrity": "sha512-UTOY+59K6IA94tec8Wjqm0FSh5OVudGNB0NL/P6fB3HiE3bYOY3VYBGijsnOHNkQSwC1FKkU77pmq7xp9CskLw==",
+      "dev": true,
+      "dependencies": {
+        "graceful-fs": "^4.2.8",
+        "streamx": "^2.12.0"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
     "node_modules/fs.realpath": {
       "version": "1.0.0",
       "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz",
@@ -8236,6 +8408,37 @@
         "node": ">= 6"
       }
     },
+    "node_modules/glob-stream": {
+      "version": "8.0.0",
+      "resolved": "https://registry.npmjs.org/glob-stream/-/glob-stream-8.0.0.tgz",
+      "integrity": "sha512-CdIUuwOkYNv9ZadR3jJvap8CMooKziQZ/QCSPhEb7zqfsEI5YnPmvca7IvbaVE3z58ZdUYD2JsU6AUWjL8WZJA==",
+      "dev": true,
+      "dependencies": {
+        "@gulpjs/to-absolute-glob": "^4.0.0",
+        "anymatch": "^3.1.3",
+        "fastq": "^1.13.0",
+        "glob-parent": "^6.0.2",
+        "is-glob": "^4.0.3",
+        "is-negated-glob": "^1.0.0",
+        "normalize-path": "^3.0.0",
+        "streamx": "^2.12.5"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
+    "node_modules/glob-stream/node_modules/glob-parent": {
+      "version": "6.0.2",
+      "resolved": "https://registry.npmjs.org/glob-parent/-/glob-parent-6.0.2.tgz",
+      "integrity": "sha512-XxwI8EOhVQgWp6iDL+3b0r86f4d6AX6zSU55HfB4ydCEuXLXc5FcYeOu+nnGftS4TEju/11rt4KJPTMgbfmv4A==",
+      "dev": true,
+      "dependencies": {
+        "is-glob": "^4.0.3"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
     "node_modules/glob-to-regexp": {
       "version": "0.4.1",
       "resolved": "https://registry.npmjs.org/glob-to-regexp/-/glob-to-regexp-0.4.1.tgz",
@@ -8267,6 +8470,15 @@
       "resolved": "https://registry.npmjs.org/graceful-fs/-/graceful-fs-4.2.11.tgz",
       "integrity": "sha512-RbJ5/jmFcNNCcDV5o9eTnBLJ/HszWV0P73bc+Ff4nS/rJj+YaS6IGyiOL0VoBYX+l1Wrl3k63h/KrH+nhJ0XvQ=="
     },
+    "node_modules/gulp-sort": {
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/gulp-sort/-/gulp-sort-2.0.0.tgz",
+      "integrity": "sha512-MyTel3FXOdh1qhw1yKhpimQrAmur9q1X0ZigLmCOxouQD+BD3za9/89O+HfbgBQvvh4igEbp0/PUWO+VqGYG1g==",
+      "dev": true,
+      "dependencies": {
+        "through2": "^2.0.1"
+      }
+    },
     "node_modules/har-schema": {
       "version": "2.0.0",
       "resolved": "https://registry.npmjs.org/har-schema/-/har-schema-2.0.0.tgz",
@@ -8642,6 +8854,152 @@
         "@babel/runtime": "^7.23.2"
       }
     },
+    "node_modules/i18next-http-backend": {
+      "version": "2.5.0",
+      "resolved": "https://registry.npmjs.org/i18next-http-backend/-/i18next-http-backend-2.5.0.tgz",
+      "integrity": "sha512-Z/aQsGZk1gSxt2/DztXk92DuDD20J+rNudT7ZCdTrNOiK8uQppfvdjq9+DFQfpAnFPn3VZS+KQIr1S/W1KxhpQ==",
+      "dependencies": {
+        "cross-fetch": "4.0.0"
+      }
+    },
+    "node_modules/i18next-scanner": {
+      "version": "4.4.0",
+      "resolved": "https://registry.npmjs.org/i18next-scanner/-/i18next-scanner-4.4.0.tgz",
+      "integrity": "sha512-bgnVEfoFHLVxfXNQtsFFzexB/5kwgDZZkZ6+AnCmyaFKEQQbtMkgPgLHlMZ0deIIEG6KN/tYAus5ZJzng2Ac9g==",
+      "dev": true,
+      "dependencies": {
+        "acorn": "^8.0.4",
+        "acorn-jsx": "^5.3.1",
+        "acorn-stage3": "^4.0.0",
+        "acorn-walk": "^8.0.0",
+        "chalk": "^4.1.0",
+        "clone-deep": "^4.0.0",
+        "commander": "^9.0.0",
+        "deepmerge": "^4.0.0",
+        "ensure-type": "^1.5.0",
+        "eol": "^0.9.1",
+        "esprima-next": "^5.7.0",
+        "gulp-sort": "^2.0.0",
+        "i18next": "*",
+        "lodash": "^4.0.0",
+        "parse5": "^6.0.0",
+        "sortobject": "^4.0.0",
+        "through2": "^4.0.0",
+        "vinyl": "^3.0.0",
+        "vinyl-fs": "^4.0.0"
+      },
+      "bin": {
+        "i18next-scanner": "bin/cli.js"
+      },
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/i18next-scanner-typescript": {
+      "version": "1.2.0",
+      "resolved": "https://registry.npmjs.org/i18next-scanner-typescript/-/i18next-scanner-typescript-1.2.0.tgz",
+      "integrity": "sha512-Q9VFw8LygB8cW9/ixVf6DHkrP8CD0hRvJcxpaFVGbx9HU84yYWO7PmPfEc9kMFMVjR8HtRiP2U0i8Vinb/wsww==",
+      "dependencies": {
+        "typescript": "^5.3.2"
+      }
+    },
+    "node_modules/i18next-scanner-typescript/node_modules/typescript": {
+      "version": "5.4.3",
+      "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.4.3.tgz",
+      "integrity": "sha512-KrPd3PKaCLr78MalgiwJnA25Nm8HAmdwN3mYUYZgG/wizIo9EainNVQI9/yDavtVFRN2h3k8uf3GLHuhDMgEHg==",
+      "bin": {
+        "tsc": "bin/tsc",
+        "tsserver": "bin/tsserver"
+      },
+      "engines": {
+        "node": ">=14.17"
+      }
+    },
+    "node_modules/i18next-scanner/node_modules/ansi-styles": {
+      "version": "4.3.0",
+      "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz",
+      "integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==",
+      "dev": true,
+      "dependencies": {
+        "color-convert": "^2.0.1"
+      },
+      "engines": {
+        "node": ">=8"
+      },
+      "funding": {
+        "url": "https://github.com/chalk/ansi-styles?sponsor=1"
+      }
+    },
+    "node_modules/i18next-scanner/node_modules/chalk": {
+      "version": "4.1.2",
+      "resolved": "https://registry.npmjs.org/chalk/-/chalk-4.1.2.tgz",
+      "integrity": "sha512-oKnbhFyRIXpUuez8iBMmyEa4nbj4IOQyuhc/wy9kY7/WVPcwIO9VA668Pu8RkO7+0G76SLROeyw9CpQ061i4mA==",
+      "dev": true,
+      "dependencies": {
+        "ansi-styles": "^4.1.0",
+        "supports-color": "^7.1.0"
+      },
+      "engines": {
+        "node": ">=10"
+      },
+      "funding": {
+        "url": "https://github.com/chalk/chalk?sponsor=1"
+      }
+    },
+    "node_modules/i18next-scanner/node_modules/color-convert": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz",
+      "integrity": "sha512-RRECPsj7iu/xb5oKYcsFHSppFNnsj/52OVTRKb4zP5onXwVF3zVmmToNcOfGC+CRDpfK/U584fMg38ZHCaElKQ==",
+      "dev": true,
+      "dependencies": {
+        "color-name": "~1.1.4"
+      },
+      "engines": {
+        "node": ">=7.0.0"
+      }
+    },
+    "node_modules/i18next-scanner/node_modules/color-name": {
+      "version": "1.1.4",
+      "resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz",
+      "integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==",
+      "dev": true
+    },
+    "node_modules/i18next-scanner/node_modules/has-flag": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/has-flag/-/has-flag-4.0.0.tgz",
+      "integrity": "sha512-EykJT/Q1KjTWctppgIAgfSO0tKVuZUjhgMr17kqTumMl6Afv3EISleU7qZUzoXDFTAHTDC4NOoG/ZxU3EvlMPQ==",
+      "dev": true,
+      "engines": {
+        "node": ">=8"
+      }
+    },
+    "node_modules/i18next-scanner/node_modules/parse5": {
+      "version": "6.0.1",
+      "resolved": "https://registry.npmjs.org/parse5/-/parse5-6.0.1.tgz",
+      "integrity": "sha512-Ofn/CTFzRGTTxwpNEs9PP93gXShHcTq255nzRYSKe8AkVpZY7e1fpmTfOyoIvjP5HG7Z2ZM7VS9PPhQGW2pOpw==",
+      "dev": true
+    },
+    "node_modules/i18next-scanner/node_modules/supports-color": {
+      "version": "7.2.0",
+      "resolved": "https://registry.npmjs.org/supports-color/-/supports-color-7.2.0.tgz",
+      "integrity": "sha512-qpCAvRl9stuOHveKsn7HncJRvv501qIacKzQlO/+Lwxc9+0q2wLyv4Dfvt80/DPn2pqOBsJdDiogXGR9+OvwRw==",
+      "dev": true,
+      "dependencies": {
+        "has-flag": "^4.0.0"
+      },
+      "engines": {
+        "node": ">=8"
+      }
+    },
+    "node_modules/i18next-scanner/node_modules/through2": {
+      "version": "4.0.2",
+      "resolved": "https://registry.npmjs.org/through2/-/through2-4.0.2.tgz",
+      "integrity": "sha512-iOqSav00cVxEEICeD7TjLB1sueEL+81Wpzp2bY17uZjZN0pWZPuo4suZ/61VujxmqSGFfgOcNuTZ85QJwNZQpw==",
+      "dev": true,
+      "dependencies": {
+        "readable-stream": "3"
+      }
+    },
     "node_modules/iconv-lite": {
       "version": "0.4.24",
       "resolved": "https://registry.npmjs.org/iconv-lite/-/iconv-lite-0.4.24.tgz",
@@ -8991,6 +9349,15 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
+    "node_modules/is-negated-glob": {
+      "version": "1.0.0",
+      "resolved": "https://registry.npmjs.org/is-negated-glob/-/is-negated-glob-1.0.0.tgz",
+      "integrity": "sha512-czXVVn/QEmgvej1f50BZ648vUI+em0xqMq2Sn+QncCLN4zj1UAxlT+kw/6ggQTOaZPd1HqKQGEqbpQVtJucWug==",
+      "dev": true,
+      "engines": {
+        "node": ">=0.10.0"
+      }
+    },
     "node_modules/is-number": {
       "version": "7.0.0",
       "resolved": "https://registry.npmjs.org/is-number/-/is-number-7.0.0.tgz",
@@ -9130,6 +9497,15 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
+    "node_modules/is-valid-glob": {
+      "version": "1.0.0",
+      "resolved": "https://registry.npmjs.org/is-valid-glob/-/is-valid-glob-1.0.0.tgz",
+      "integrity": "sha512-AhiROmoEFDSsjx8hW+5sGwgKVIORcXnrlAx/R0ZSeaPw70Vw0CqkGBBhHGL58Uox2eXnU1AnvXJl1XlyedO5bA==",
+      "dev": true,
+      "engines": {
+        "node": ">=0.10.0"
+      }
+    },
     "node_modules/is-weakmap": {
       "version": "2.0.1",
       "resolved": "https://registry.npmjs.org/is-weakmap/-/is-weakmap-2.0.1.tgz",
@@ -9878,6 +10254,15 @@
         "node": ">=6"
       }
     },
+    "node_modules/lead": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/lead/-/lead-4.0.0.tgz",
+      "integrity": "sha512-DpMa59o5uGUWWjruMp71e6knmwKU3jRBBn1kjuLWN9EeIOxNeSAwvHf03WIl8g/ZMR2oSQC9ej3yeLBwdDc/pg==",
+      "dev": true,
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
     "node_modules/lean4": {
       "version": "0.0.119",
       "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985",
@@ -12286,6 +12671,18 @@
         "node": ">=0.10.0"
       }
     },
+    "node_modules/now-and-later": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/now-and-later/-/now-and-later-3.0.0.tgz",
+      "integrity": "sha512-pGO4pzSdaxhWTGkfSfHx3hVzJVslFPwBp2Myq9MYN/ChfJZF87ochMAXnvz6/58RJSf5ik2q9tXprBBrk2cpcg==",
+      "dev": true,
+      "dependencies": {
+        "once": "^1.4.0"
+      },
+      "engines": {
+        "node": ">= 10.13.0"
+      }
+    },
     "node_modules/npm-run-path": {
       "version": "4.0.1",
       "resolved": "https://registry.npmjs.org/npm-run-path/-/npm-run-path-4.0.1.tgz",
@@ -13074,6 +13471,12 @@
         }
       ]
     },
+    "node_modules/queue-tick": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/queue-tick/-/queue-tick-1.0.1.tgz",
+      "integrity": "sha512-kJt5qhMxoszgU/62PLP1CJytzd2NKetjSRnyuj31fDd3Rlcz3fzlFdFLD1SItunPwyqEOkca6GbV612BWfaBag==",
+      "dev": true
+    },
     "node_modules/randombytes": {
       "version": "2.1.0",
       "resolved": "https://registry.npmjs.org/randombytes/-/randombytes-2.1.0.tgz",
@@ -13773,6 +14176,21 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/remove-trailing-separator": {
+      "version": "1.1.0",
+      "resolved": "https://registry.npmjs.org/remove-trailing-separator/-/remove-trailing-separator-1.1.0.tgz",
+      "integrity": "sha512-/hS+Y0u3aOfIETiaiirUFwDBDzmXPvO+jAfKTitUngIPzdKc6Z0LoFjM/CK5PL4C+eKwHohlHAb6H0VFfmmUsw==",
+      "dev": true
+    },
+    "node_modules/replace-ext": {
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/replace-ext/-/replace-ext-2.0.0.tgz",
+      "integrity": "sha512-UszKE5KVK6JvyD92nzMn9cDapSk6w/CaFZ96CnmDMUqH9oowfxF/ZjRITD25H4DnOQClLA4/j7jLGXXLVKxAug==",
+      "dev": true,
+      "engines": {
+        "node": ">= 10"
+      }
+    },
     "node_modules/request": {
       "version": "2.88.2",
       "resolved": "https://registry.npmjs.org/request/-/request-2.88.2.tgz",
@@ -13875,6 +14293,18 @@
         "node": ">=4"
       }
     },
+    "node_modules/resolve-options": {
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/resolve-options/-/resolve-options-2.0.0.tgz",
+      "integrity": "sha512-/FopbmmFOQCfsCx77BRFdKOniglTiHumLgwvd6IDPihy1GKkadZbgQJBcTb2lMzSR1pndzd96b1nZrreZ7+9/A==",
+      "dev": true,
+      "dependencies": {
+        "value-or-function": "^4.0.0"
+      },
+      "engines": {
+        "node": ">= 10.13.0"
+      }
+    },
     "node_modules/restore-cursor": {
       "version": "3.1.0",
       "resolved": "https://registry.npmjs.org/restore-cursor/-/restore-cursor-3.1.0.tgz",
@@ -14289,6 +14719,18 @@
         "tslib": "^2.0.3"
       }
     },
+    "node_modules/sortobject": {
+      "version": "4.17.0",
+      "resolved": "https://registry.npmjs.org/sortobject/-/sortobject-4.17.0.tgz",
+      "integrity": "sha512-gzx7USv55AFRQ7UCWJHHauwD/ptUHF9MLXCGO3f5M9zauDPZ/4a9H6/VVbOXefdpEoI1unwB/bArHIVMbWBHmA==",
+      "dev": true,
+      "engines": {
+        "node": ">=10"
+      },
+      "funding": {
+        "url": "https://bevry.me/fund"
+      }
+    },
     "node_modules/source-map": {
       "version": "0.5.7",
       "resolved": "https://registry.npmjs.org/source-map/-/source-map-0.5.7.tgz",
@@ -14434,6 +14876,15 @@
         "node": ">= 0.4"
       }
     },
+    "node_modules/stream-composer": {
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/stream-composer/-/stream-composer-1.0.2.tgz",
+      "integrity": "sha512-bnBselmwfX5K10AH6L4c8+S5lgZMWI7ZYrz2rvYjCPB2DIMC4Ig8OpxGpNJSxRZ58oti7y1IcNvjBAz9vW5m4w==",
+      "dev": true,
+      "dependencies": {
+        "streamx": "^2.13.2"
+      }
+    },
     "node_modules/stream-http": {
       "version": "3.2.0",
       "resolved": "https://registry.npmjs.org/stream-http/-/stream-http-3.2.0.tgz",
@@ -14445,6 +14896,19 @@
         "xtend": "^4.0.2"
       }
     },
+    "node_modules/streamx": {
+      "version": "2.16.1",
+      "resolved": "https://registry.npmjs.org/streamx/-/streamx-2.16.1.tgz",
+      "integrity": "sha512-m9QYj6WygWyWa3H1YY69amr4nVgy61xfjys7xO7kviL5rfIEc2naf+ewFiOA+aEJD7y0JO3h2GoiUv4TDwEGzQ==",
+      "dev": true,
+      "dependencies": {
+        "fast-fifo": "^1.1.0",
+        "queue-tick": "^1.0.1"
+      },
+      "optionalDependencies": {
+        "bare-events": "^2.2.0"
+      }
+    },
     "node_modules/string_decoder": {
       "version": "1.3.0",
       "resolved": "https://registry.npmjs.org/string_decoder/-/string_decoder-1.3.0.tgz",
@@ -14592,6 +15056,15 @@
         "node": ">=6"
       }
     },
+    "node_modules/teex": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/teex/-/teex-1.0.1.tgz",
+      "integrity": "sha512-eYE6iEI62Ni1H8oIa7KlDU6uQBtqr4Eajni3wX7rpfXD8ysFx8z0+dri+KWEPWpBsxXfxu58x/0jvTVT1ekOSg==",
+      "dev": true,
+      "dependencies": {
+        "streamx": "^2.12.5"
+      }
+    },
     "node_modules/temp": {
       "version": "0.8.4",
       "resolved": "https://registry.npmjs.org/temp/-/temp-0.8.4.tgz",
@@ -14749,6 +15222,18 @@
         "node": ">=8.0"
       }
     },
+    "node_modules/to-through": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/to-through/-/to-through-3.0.0.tgz",
+      "integrity": "sha512-y8MN937s/HVhEoBU1SxfHC+wxCHkV1a9gW8eAdTadYh/bGyesZIVcbjI+mSpFbSVwQici/XjBjuUyri1dnXwBw==",
+      "dev": true,
+      "dependencies": {
+        "streamx": "^2.12.5"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
     "node_modules/toidentifier": {
       "version": "1.0.1",
       "resolved": "https://registry.npmjs.org/toidentifier/-/toidentifier-1.0.1.tgz",
@@ -15351,6 +15836,15 @@
         "node": ">=6"
       }
     },
+    "node_modules/value-or-function": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/value-or-function/-/value-or-function-4.0.0.tgz",
+      "integrity": "sha512-aeVK81SIuT6aMJfNo9Vte8Dw0/FZINGBV8BfCraGtqVxIeLAEhJyoWs8SmvRVmXfGss2PmmOwZCuBPbZR+IYWg==",
+      "dev": true,
+      "engines": {
+        "node": ">= 10.13.0"
+      }
+    },
     "node_modules/vary": {
       "version": "1.1.2",
       "resolved": "https://registry.npmjs.org/vary/-/vary-1.1.2.tgz",
@@ -15413,6 +15907,133 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/vinyl": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/vinyl/-/vinyl-3.0.0.tgz",
+      "integrity": "sha512-rC2VRfAVVCGEgjnxHUnpIVh3AGuk62rP3tqVrn+yab0YH7UULisC085+NYH+mnqf3Wx4SpSi1RQMwudL89N03g==",
+      "dev": true,
+      "dependencies": {
+        "clone": "^2.1.2",
+        "clone-stats": "^1.0.0",
+        "remove-trailing-separator": "^1.1.0",
+        "replace-ext": "^2.0.0",
+        "teex": "^1.0.1"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
+    "node_modules/vinyl-contents": {
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/vinyl-contents/-/vinyl-contents-2.0.0.tgz",
+      "integrity": "sha512-cHq6NnGyi2pZ7xwdHSW1v4Jfnho4TEGtxZHw01cmnc8+i7jgR6bRnED/LbrKan/Q7CvVLbnvA5OepnhbpjBZ5Q==",
+      "dev": true,
+      "dependencies": {
+        "bl": "^5.0.0",
+        "vinyl": "^3.0.0"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
+    "node_modules/vinyl-contents/node_modules/bl": {
+      "version": "5.1.0",
+      "resolved": "https://registry.npmjs.org/bl/-/bl-5.1.0.tgz",
+      "integrity": "sha512-tv1ZJHLfTDnXE6tMHv73YgSJaWR2AFuPwMntBe7XL/GBFHnT0CLnsHMogfk5+GzCDC5ZWarSCYaIGATZt9dNsQ==",
+      "dev": true,
+      "dependencies": {
+        "buffer": "^6.0.3",
+        "inherits": "^2.0.4",
+        "readable-stream": "^3.4.0"
+      }
+    },
+    "node_modules/vinyl-contents/node_modules/buffer": {
+      "version": "6.0.3",
+      "resolved": "https://registry.npmjs.org/buffer/-/buffer-6.0.3.tgz",
+      "integrity": "sha512-FTiCpNxtwiZZHEZbcbTIcZjERVICn9yq/pDFkTl95/AxzD1naBctN7YO68riM/gLSDY7sdrMby8hofADYuuqOA==",
+      "dev": true,
+      "funding": [
+        {
+          "type": "github",
+          "url": "https://github.com/sponsors/feross"
+        },
+        {
+          "type": "patreon",
+          "url": "https://www.patreon.com/feross"
+        },
+        {
+          "type": "consulting",
+          "url": "https://feross.org/support"
+        }
+      ],
+      "dependencies": {
+        "base64-js": "^1.3.1",
+        "ieee754": "^1.2.1"
+      }
+    },
+    "node_modules/vinyl-fs": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/vinyl-fs/-/vinyl-fs-4.0.0.tgz",
+      "integrity": "sha512-7GbgBnYfaquMk3Qu9g22x000vbYkOex32930rBnc3qByw6HfMEAoELjCjoJv4HuEQxHAurT+nvMHm6MnJllFLw==",
+      "dev": true,
+      "dependencies": {
+        "fs-mkdirp-stream": "^2.0.1",
+        "glob-stream": "^8.0.0",
+        "graceful-fs": "^4.2.11",
+        "iconv-lite": "^0.6.3",
+        "is-valid-glob": "^1.0.0",
+        "lead": "^4.0.0",
+        "normalize-path": "3.0.0",
+        "resolve-options": "^2.0.0",
+        "stream-composer": "^1.0.2",
+        "streamx": "^2.14.0",
+        "to-through": "^3.0.0",
+        "value-or-function": "^4.0.0",
+        "vinyl": "^3.0.0",
+        "vinyl-sourcemap": "^2.0.0"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
+    "node_modules/vinyl-fs/node_modules/iconv-lite": {
+      "version": "0.6.3",
+      "resolved": "https://registry.npmjs.org/iconv-lite/-/iconv-lite-0.6.3.tgz",
+      "integrity": "sha512-4fCk79wshMdzMp2rH06qWrJE4iolqLhCUH+OiuIgU++RB0+94NlDL81atO7GX55uUKueo0txHNtvEyI6D7WdMw==",
+      "dev": true,
+      "dependencies": {
+        "safer-buffer": ">= 2.1.2 < 3.0.0"
+      },
+      "engines": {
+        "node": ">=0.10.0"
+      }
+    },
+    "node_modules/vinyl-sourcemap": {
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/vinyl-sourcemap/-/vinyl-sourcemap-2.0.0.tgz",
+      "integrity": "sha512-BAEvWxbBUXvlNoFQVFVHpybBbjW1r03WhohJzJDSfgrrK5xVYIDTan6xN14DlyImShgDRv2gl9qhM6irVMsV0Q==",
+      "dev": true,
+      "dependencies": {
+        "convert-source-map": "^2.0.0",
+        "graceful-fs": "^4.2.10",
+        "now-and-later": "^3.0.0",
+        "streamx": "^2.12.5",
+        "vinyl": "^3.0.0",
+        "vinyl-contents": "^2.0.0"
+      },
+      "engines": {
+        "node": ">=10.13.0"
+      }
+    },
+    "node_modules/vinyl/node_modules/clone": {
+      "version": "2.1.2",
+      "resolved": "https://registry.npmjs.org/clone/-/clone-2.1.2.tgz",
+      "integrity": "sha512-3Pe/CF1Nn94hyhIYpjtiLhdCoEoz0DqQ+988E9gmeEdQZlojxnOb74wctFyuwWQHzqyf9X7C7MG8juUpqBJT8w==",
+      "dev": true,
+      "engines": {
+        "node": ">=0.8"
+      }
+    },
     "node_modules/vite": {
       "version": "4.5.2",
       "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.2.tgz",

package.json

@@ -28,6 +28,8 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "i18next": "^23.10.1",
+    "i18next-http-backend": "^2.5.0",
+    "i18next-scanner-typescript": "^1.2.0",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
     "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
     "octokit": "^3.1.2",
@@ -61,6 +63,7 @@
     "concurrently": "^7.6.0",
     "css-loader": "^6.7.3",
     "file-loader": "^6.2.0",
+    "i18next-scanner": "^4.4.0",
     "nodemon": "^3.0.1",
     "react-refresh": "^0.14.0",
     "style-loader": "^3.3.1",
@@ -76,7 +79,8 @@
     "preview": "vite preview",
     "build_server": "cd server && lake build",
     "build_client": "cross-env NODE_ENV=production vite build",
-    "production": "cross-env NODE_ENV=production node relay/index.mjs"
+    "production": "cross-env NODE_ENV=production node relay/index.mjs",
+    "translate": "npx i18next-scanner --config client/i18next-scanner.config.cjs"
   },
   "eslintConfig": {
     "extends": [