refactor: navigation and other stuff

This commit is contained in:
Jon Eugster
2024-05-16 02:31:41 +02:00
parent 08875e4415
commit d82ef8af8f
35 changed files with 1049 additions and 587 deletions
+35 -10
View File
@@ -1,5 +1,6 @@
import * as React from 'react';
import { Outlet, useParams } from "react-router-dom";
import { useEffect, useState } from 'react';
import '@fontsource/roboto/300.css';
import '@fontsource/roboto/400.css';
@@ -8,31 +9,55 @@ import '@fontsource/roboto/700.css';
import './css/reset.css';
import './css/app.css';
import { PreferencesContext} from './components/infoview/context';
import { PageContext, PopupContext, PreferencesContext} from './components/infoview/context';
import UsePreferences from "./state/hooks/use_preferences"
import i18n from './i18n';
import { Navigation } from './components/navigation';
import { useSelector } from 'react-redux';
import { changeTypewriterMode, selectTypewriterMode } from './state/progress';
import { useAppDispatch } from './hooks';
import { Popup } from './components/popup/popup';
export const GameIdContext = React.createContext<string>(undefined);
export const GameIdContext = React.createContext<{
gameId: string,
worldId: string|null,
levelId: number|null}>({gameId: null, worldId: null, levelId: null});
function App() {
const params = useParams()
const gameId = "g/" + params.owner + "/" + params.repo
const gameId = (params.owner && params.repo) ? "g/" + params.owner + "/" + params.repo : null
const worldId = params.worldId
const levelId = parseInt(params.levelId)
const {mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = UsePreferences()
React.useEffect(() => {
const dispatch = useAppDispatch()
const typewriterMode = useSelector(selectTypewriterMode(gameId))
const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
const [lockEditorMode, setLockEditorMode] = useState(false)
const [typewriterInput, setTypewriterInput] = useState("")
const [page, setPage] = useState(0)
const [popupContent, setPopupContent] = useState(null)
useEffect(() => {
i18n.changeLanguage(language)
}, [language])
return (
<div className="app">
<GameIdContext.Provider value={gameId}>
<PreferencesContext.Provider value={{mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}}>
<React.Suspense>
<Outlet />
</React.Suspense>
</PreferencesContext.Provider>
<GameIdContext.Provider value={{gameId, worldId, levelId}}>
<PreferencesContext.Provider value={{mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}}>
<PopupContext.Provider value={{popupContent, setPopupContent}}>
<PageContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode, page, setPage}}>
<Navigation />
<React.Suspense>
<Outlet />
</React.Suspense>
</PageContext.Provider>
{ popupContent && <Popup /> }
</PopupContext.Provider>
</PreferencesContext.Provider>
</GameIdContext.Provider>
</div>
)
-321
View File
@@ -1,321 +0,0 @@
/**
* @file contains the navigation bars of the app.
*/
import * as React from 'react'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
faArrowRight, faArrowLeft, faXmark, faBars, faCode,
faCircleInfo, faTerminal, faGear } from '@fortawesome/free-solid-svg-icons'
import { GameIdContext } from "../app"
import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context"
import { GameInfo, useGetGameInfoQuery } from '../state/api'
import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
import { useAppDispatch, useAppSelector } from '../hooks'
import { Button } from './button'
import { downloadProgress } from './popup/erase'
import { useTranslation } from 'react-i18next'
/** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */
function MobileNavButtons({pageNumber, setPageNumber}:
{ pageNumber: number,
setPageNumber: any}) {
const gameId = React.useContext(GameIdContext)
const { t } = useTranslation()
const dispatch = useAppDispatch()
// if `prevText` or `prevIcon` is set, show a button to go back
let prevText = {0: null, 1: t("Intro"), 2: null}[pageNumber]
let prevIcon = {0: null, 1: null, 2: faBookOpen}[pageNumber]
let prevTitle = {0: null, 1: t("Game Introduction"), 2: t("World selection")}[pageNumber]
// if `nextText` or `nextIcon` is set, show a button to go forward
let nextText = {0: t("Start"), 1: null, 2: null}[pageNumber]
let nextIcon = {0: null, 1: faBook, 2: null}[pageNumber]
let nextTitle = {0: t("World selection"), 1: t("Inventory"), 2: null}[pageNumber]
return <>
{(prevText || prevIcon) &&
<Button className="btn btn-inverted toggle-width" to={pageNumber == 0 ? "/" : ""}
inverted="true" title={prevTitle}
onClick={() => {pageNumber == 0 ? null : setPageNumber(pageNumber - 1)}}>
{prevIcon && <FontAwesomeIcon icon={prevIcon} />}
{prevText && `${prevText}`}
</Button>
}
{(nextText || nextIcon) &&
<Button className="btn btn-inverted toggle-width" to="" inverted="true"
title={nextTitle} onClick={() => {
console.log(`page number: ${pageNumber}`)
setPageNumber(pageNumber+1);
dispatch(changedOpenedIntro({game: gameId, openedIntro: true}))}}>
{nextText && `${nextText}`}
{nextIcon && <FontAwesomeIcon icon={nextIcon} />}
</Button>
}
</>
}
/** button to toggle dropdown menu. */
export function MenuButton({navOpen, setNavOpen}) {
return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}>
{navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
</Button>
}
/** button to go one level futher.
* for the last level, this button turns into a button going back to the welcome page.
*/
function NextButton({worldSize, difficulty, completed, setNavOpen}) {
const { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
return (levelId < worldSize ?
<Button inverted="true"
to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title={t("next level")}
disabled={difficulty >= 2 && !(completed || levelId == 0)}
onClick={() => setNavOpen(false)}>
<FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? t("Next") : t("Start")}
</Button>
:
<Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
<FontAwesomeIcon icon={faHome} />&nbsp;{t("Leave World")}
</Button>
)
}
/** button to go one level back.
* only renders if the current level id is > 0.
*/
function PreviousButton({setNavOpen}) {
const { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
return (levelId > 0 && <>
<Button disabled={levelId <= 0} inverted="true"
to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
title={t("previous level")}
onClick={() => setNavOpen(false)}>
<FontAwesomeIcon icon={faArrowLeft} />&nbsp;{t("Previous")}
</Button>
</>)
}
/** button to toggle between editor and typewriter */
function InputModeButton({setNavOpen, isDropdown}) {
const { t } = useTranslation()
const {levelId} = React.useContext(WorldLevelIdContext)
const {typewriterMode, setTypewriterMode, lockEditorMode} = React.useContext(InputModeContext)
/** toggle input mode if allowed */
function toggleInputMode(ev: React.MouseEvent) {
if (!lockEditorMode){
setTypewriterMode(!typewriterMode)
setNavOpen(false)
}
}
return <Button
className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockEditorMode}
inverted="true" to=""
onClick={(ev) => toggleInputMode(ev)}
title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")}>
<FontAwesomeIcon icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal} />
{isDropdown && ((typewriterMode && !lockEditorMode) ? <>&nbsp;{t("Editor mode")}</> : <>&nbsp;{t("Typewriter mode")}</>)}
</Button>
}
export function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
const { t } = useTranslation()
return <Button className="btn btn-inverted"
title={t("Impressum")} inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
<FontAwesomeIcon icon={faCircleInfo} />
{isDropdown && <>&nbsp;{t("Impressum")}</>}
</Button>
}
export function PrivacyButton({setNavOpen, togglePrivacy, isDropdown}) {
const { t } = useTranslation()
return <Button className="btn btn-inverted"
title={t("Privacy Policy")} inverted="true" to="" onClick={(ev) => {togglePrivacy(ev); setNavOpen(false)}}>
<FontAwesomeIcon icon={faCircleInfo} />
{isDropdown && <>&nbsp;{t("Privacy Policy")}</>}
</Button>
}
export function PreferencesButton({setNavOpen, togglePreferencesPopup}) {
const { t } = useTranslation()
return <Button title={t("Preferences")} inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
<FontAwesomeIcon icon={faGear} />&nbsp;{t("Preferences")}
</Button>
}
function GameInfoButton({setNavOpen, toggleInfo}) {
const { t } = useTranslation()
return <Button className="btn btn-inverted"
title={t("Game Info & Credits")} inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
<FontAwesomeIcon icon={faCircleInfo} />&nbsp;{t("Game Info")}
</Button>
}
function EraseButton ({setNavOpen, toggleEraseMenu}) {
const { t } = useTranslation()
return <Button title={t("Clear Progress")} inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
<FontAwesomeIcon icon={faEraser} />&nbsp;{t("Erase")}
</Button>
}
function DownloadButton ({setNavOpen, gameId, gameProgress}) {
const { t } = useTranslation()
return <Button title={t("Download Progress")} inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
<FontAwesomeIcon icon={faDownload} />&nbsp;{t("Download")}
</Button>
}
function UploadButton ({setNavOpen, toggleUploadMenu}) {
const { t } = useTranslation()
return <Button title={t("Load Progress from JSON")} inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
<FontAwesomeIcon icon={faUpload} />&nbsp;{t("Upload")}
</Button>
}
/** button to go back to welcome page */
function HomeButton({isDropdown}) {
const { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
return <Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
<FontAwesomeIcon icon={faHome} />
{isDropdown && <>&nbsp;{t("Home")}</>}
</Button>
}
function LandingPageButton() {
const { t } = useTranslation()
return <Button inverted="false" title={t("back to games selection")} to="/">
<FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
</Button>
}
/** button in mobile level to toggle inventory.
* only displays a button if `setPageNumber` is set.
*/
function InventoryButton({pageNumber, setPageNumber}) {
const { t } = useTranslation()
return (setPageNumber &&
<Button to="" className="btn btn-inverted toggle-width"
title={pageNumber ? t("close inventory") : t("show inventory")}
inverted="true" onClick={() => {setPageNumber(pageNumber ? 0 : 1)}}>
<FontAwesomeIcon icon={pageNumber ? faBookOpen : faBook} />
</Button>
)
}
/** the navigation bar on the welcome page */
export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, togglePrivacy, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
pageNumber: number,
setPageNumber: any,
gameInfo: GameInfo,
toggleImpressum: any,
togglePrivacy: any,
toggleEraseMenu: any,
toggleUploadMenu: any,
toggleInfo: any,
togglePreferencesPopup: () => void;
}) {
const { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const gameProgress = useAppSelector(selectProgress(gameId))
const {mobile} = React.useContext(PreferencesContext)
const [navOpen, setNavOpen] = React.useState(false)
return <div className="app-bar">
<div className='app-bar-left'>
<LandingPageButton />
<span className="app-bar-title"></span>
</div>
<div>
{!mobile && <span className="app-bar-title">{t(gameInfo?.title, {ns: gameId})}</span>}
</div>
<div className="nav-btns">
{mobile && <MobileNavButtons pageNumber={pageNumber} setPageNumber={setPageNumber} />}
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen} />
</div>
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
<EraseButton setNavOpen={setNavOpen} toggleEraseMenu={toggleEraseMenu}/>
<DownloadButton setNavOpen={setNavOpen} gameId={gameId} gameProgress={gameProgress}/>
<UploadButton setNavOpen={setNavOpen} toggleUploadMenu={toggleUploadMenu}/>
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
<PrivacyButton setNavOpen={setNavOpen} togglePrivacy={togglePrivacy} isDropdown={true} />
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
</div>
</div>
}
/** the navigation bar in a level */
export function LevelAppBar({isLoading, levelTitle, toggleImpressum, togglePrivacy, toggleInfo, togglePreferencesPopup, pageNumber=undefined, setPageNumber=undefined} : {
isLoading: boolean,
levelTitle: string,
toggleImpressum: any,
togglePrivacy: any,
toggleInfo: any,
togglePreferencesPopup: any,
pageNumber?: number,
setPageNumber?: any,
}) {
const { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
const {mobile} = React.useContext(PreferencesContext)
const [navOpen, setNavOpen] = React.useState(false)
const gameInfo = useGetGameInfoQuery({game: gameId})
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
const difficulty = useAppSelector(selectDifficulty(gameId))
let worldTitle = gameInfo.data?.worlds.nodes[worldId].title
return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
{mobile ?
<>
{/* MOBILE VERSION */}
<div>
<span className="app-bar-title">{levelTitle}</span>
</div>
<div className="nav-btns">
<InventoryButton pageNumber={pageNumber} setPageNumber={setPageNumber}/>
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
</div>
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
<NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
<PreviousButton setNavOpen={setNavOpen} />
<HomeButton isDropdown={true} />
<InputModeButton setNavOpen={setNavOpen} isDropdown={true}/>
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
<PrivacyButton setNavOpen={setNavOpen} togglePrivacy={togglePrivacy} isDropdown={true} />
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
</div>
</> :
<>
{/* DESKTOP VERSION */}
<div className='app-bar-left'>
<HomeButton isDropdown={false} />
<span className="app-bar-title">{worldTitle && `${t("World")}: ${t(worldTitle, {ns: gameId})}`}</span>
</div>
<div>
<span className="app-bar-title">{levelTitle}</span>
</div>
<div className="nav-btns">
<PreviousButton setNavOpen={setNavOpen} />
<NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
<InputModeButton setNavOpen={setNavOpen} isDropdown={false}/>
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
</div>
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
<PrivacyButton setNavOpen={setNavOpen} togglePrivacy={togglePrivacy} isDropdown={true} />
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
</div>
</>
}
</div>
}
+2 -2
View File
@@ -11,8 +11,8 @@ export default function ErrorPage() {
<div className="error-message">
<h1>Oops!</h1>
<p>Something unexpected happened:</p>
<p><code>{error.statusText || error.message}</code></p>
<p>Please create an issue on the <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">lean4game repo</a>.</p>
<p><code>({error.status}) {error.statusText || error.message}<br/>{error.data}</code></p>
<p>Please create an issue at the <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">lean4game repo</a>.</p>
<div className="thought-bubble" />
<div className="thought-bubble" />
<div className="thought-bubble" />
+16
View File
@@ -0,0 +1,16 @@
import i18next from "i18next"
import React from "react"
import { useParams } from "react-router-dom"
import { GameIdContext } from "../app"
import { useGetGameInfoQuery } from "../state/api"
function Game() {
const params = useParams()
const levelId = parseInt(params.levelId)
const worldId = params.worldId
return <div>
<GameIdContext.Provider value={gameId}></GameIdContext.Provider>
</div>
}
+1 -1
View File
@@ -12,7 +12,7 @@ import { GameIdContext } from "../app";
* and have the variables substituted just before displaying.
*/
function getHintText(hint: GameHint): string {
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
let { t } = useTranslation()
if (hint.rawText) {
// Replace the variable names used in the hint with the ones used by the player
+20
View File
@@ -123,6 +123,26 @@ export const DeletedChatContext = React.createContext<{
setShowHelp: () => {}
})
export const PageContext = React.createContext<{
typewriterMode: boolean,
setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
typewriterInput: string,
setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
lockEditorMode: boolean,
setLockEditorMode: React.Dispatch<React.SetStateAction<boolean>>,
page: number, /* only for mobile */
setPage: React.Dispatch<React.SetStateAction<number>>,
}>({
typewriterMode: true,
setTypewriterMode: () => {},
typewriterInput: "",
setTypewriterInput: () => {},
lockEditorMode: false,
setLockEditorMode: () => {},
page: 0,
setPage: () => {}
});
export const InputModeContext = React.createContext<{
typewriterMode: boolean,
setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
+1 -1
View File
@@ -9,7 +9,7 @@ import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infov
import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
import { InputModeContext } from './context';
import { PageContext } from './context';
import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api';
import { RpcSessionAtPos } from '@leanprover/infoview/*';
import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
+10 -10
View File
@@ -27,7 +27,7 @@ import Markdown from '../markdown';
import { Infos } from './infos';
import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
import { DeletedChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
import { InteractiveDiagnostic } from '@leanprover/infoview/*';
import { Button } from '../button';
@@ -46,7 +46,7 @@ import path from 'path';
*/
export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize }) {
const ec = React.useContext(EditorContext)
const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
const { typewriterMode, lockEditorMode } = React.useContext(PageContext)
return <>
<div className={(typewriterMode && !lockEditorMode) ? 'hidden' : ''}>
<ExerciseStatement data={level} showLeanStatement={true} />
@@ -63,8 +63,8 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
/** The part of the two editors that needs the editor connection first */
function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: string, levelId: number, level: LevelInfo, worldSize: number }) {
const ec = React.useContext(EditorContext)
const gameId = React.useContext(GameIdContext)
const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
const {gameId} = React.useContext(GameIdContext)
const { typewriterMode, lockEditorMode } = React.useContext(PageContext)
const {proof, setProof} = React.useContext(ProofContext)
@@ -137,7 +137,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
*/
function ExerciseStatement({ data, showLeanStatement = false }) {
let { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
if (!(data?.descrText || data?.descrFormat)) { return <></> }
return <>
@@ -162,7 +162,7 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
export function Main(props: { world: string, level: number, data: LevelInfo}) {
let { t } = useTranslation()
const ec = React.useContext(EditorContext);
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
const { proof, setProof } = React.useContext(ProofContext)
@@ -314,7 +314,7 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
// message = diag.message
// }
// const { typewriterMode } = React.useContext(InputModeContext)
// const { typewriterMode } = React.useContext(PageContext)
// return (
// // <details open>
@@ -369,7 +369,7 @@ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofSte
// Splitting up Typewriter into two parts is a HACK
export function TypewriterInterfaceWrapper(props: { world: string, level: number, data: LevelInfo, worldSize: number }) {
const ec = React.useContext(EditorContext)
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
useClientNotificationEffect(
'textDocument/didClose',
@@ -403,7 +403,7 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
export function TypewriterInterface({props}) {
let { t } = useTranslation()
const ec = React.useContext(EditorContext)
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const editor = React.useContext(MonacoEditorContext)
const model = editor.getModel()
const uri = model.uri.toString()
@@ -418,7 +418,7 @@ export function TypewriterInterface({props}) {
const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
const {mobile} = React.useContext(PreferencesContext)
const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext)
const { setTypewriterInput } = React.useContext(InputModeContext)
const { setTypewriterInput } = React.useContext(PageContext)
const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
const proofPanelRef = React.useRef<HTMLDivElement>(null)
+2 -2
View File
@@ -10,7 +10,7 @@ import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/co
import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer'
import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'
import { InputModeContext } from './context'
import { PageContext } from './context'
import { useTranslation } from 'react-i18next'
interface MessageViewProps {
@@ -80,7 +80,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
message = diag.message
}
const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
const { typewriterMode, lockEditorMode } = React.useContext(PageContext)
return (
// <details open>
@@ -17,7 +17,7 @@ import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } fro
import { Diagnostic } from 'vscode-languageserver-types';
import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext } from './context'
import { DeletedChatContext, PageContext, MonacoEditorContext, ProofContext } from './context'
import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
import { GameHint, ProofState } from './rpc_api'
import { useTranslation } from 'react-i18next'
@@ -87,7 +87,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
const [processing, setProcessing] = useState(false)
const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
const {typewriterInput, setTypewriterInput} = React.useContext(PageContext)
const inputRef = useRef()
+3 -3
View File
@@ -64,7 +64,7 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
// TODO: `level` is only used in the `useEffect` below to check if a new level has
// been loaded. Is there a better way to observe this?
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
const difficulty = useSelector(selectDifficulty(gameId))
@@ -147,7 +147,7 @@ return <div className={`item ${className}${enableAll ? ' enabled' : ''}${recent
}
export function Documentation({name, type, handleClose}) {
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const doc = useLoadDocQuery({game: gameId, type: type, name: name})
return <div className="documentation">
@@ -161,7 +161,7 @@ export function Documentation({name, type, handleClose}) {
/** The panel (on the welcome page) showing the user's inventory with tactics, definitions, and lemmas */
export function InventoryPanel({levelInfo, visible = true}) {
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab)
+6 -43
View File
@@ -11,27 +11,14 @@ import '../css/landing_page.css'
import bgImage from '../assets/bg.jpg'
import Markdown from './markdown';
import {PrivacyPolicyPopup, ImpressumPopup} from './popup/privacy_policy'
import { GameTile, useGetGameInfoQuery } from '../state/api'
import path from 'path';
import { PreferencesPopup } from './popup/preferences';
import { ImpressumButton, MenuButton, PreferencesButton, PrivacyButton } from './app_bar';
import ReactCountryFlag from 'react-country-flag';
import lean4gameConfig from '../config.json'
import i18next from 'i18next';
function GithubIcon({url='https://github.com'}) {
let { t } = useTranslation()
return <div className="github-link">
<a title={t("view the Lean game server on Github")} href={url}>
<svg height="24" aria-hidden="true" viewBox="0 0 16 16" version="1.1" width="24" className="">
<path fill="#fff" d="M8 0c4.42 0 8 3.58 8 8a8.013 8.013 0 0 1-5.45 7.59c-.4.08-.55-.17-.55-.38 0-.27.01-1.13.01-2.2 0-.75-.25-1.23-.54-1.48 1.78-.2 3.65-.88 3.65-3.95 0-.88-.31-1.59-.82-2.15.08-.2.36-1.02-.08-2.12 0 0-.67-.22-2.2.82-.64-.18-1.32-.27-2-.27-.68 0-1.36.09-2 .27-1.53-1.03-2.2-.82-2.2-.82-.44 1.1-.16 1.92-.08 2.12-.51.56-.82 1.28-.82 2.15 0 3.06 1.86 3.75 3.64 3.95-.23.2-.44.55-.51 1.07-.46.21-1.61.55-2.33-.66-.15-.24-.6-.83-1.23-.82-.67.01-.27.38.01.53.34.19.73.9.82 1.13.16.45.68 1.31 2.69.94 0 .67.01 1.3.01 1.49 0 .21-.15.45-.55.38A7.995 7.995 0 0 1 0 8c0-4.42 3.58-8 8-8Z"></path>
</svg>
</a>
</div>
}
import { useContext } from 'react';
import { PopupContext } from './popup/popup';
function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
let { t } = useTranslation()
@@ -75,7 +62,7 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
if (lean4gameConfig.useFlags) {
return <ReactCountryFlag key={`flag-${lang}`} title={langOpt?.name} countryCode={langOpt?.flag} className="emojiFlag"/>
} else {
return <span title={langOpt?.name}>{lang}</span>
return <span key={`flag-text-${lang}`} title={langOpt?.name}>{lang}</span>
}
})}
</td>
@@ -89,19 +76,7 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
function LandingPage() {
const navigate = useNavigate();
const [impressumPopup, setImpressumPopup] = React.useState(false);
const [privacyPopup, setPrivacyPopup] = React.useState(false);
const [preferencesPopup, setPreferencesPopup] = React.useState(false);
const [navOpen, setNavOpen] = React.useState(false);
const openImpressum = () => setImpressumPopup(true);
const closeImpressum = () => setImpressumPopup(false);
const toggleImpressum = () => setImpressumPopup(!impressumPopup);
const openPrivacy = () => setPrivacyPopup(true);
const closePrivacy = () => setPrivacyPopup(false);
const togglePrivacy = () => setPrivacyPopup(!privacyPopup);
const closePreferencesPopup = () => setPreferencesPopup(false);
const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup);
const { setPopupContent } = useContext(PopupContext)
const { t, i18n } = useTranslation()
@@ -127,15 +102,6 @@ function LandingPage() {
return <div className="landing-page">
<header style={{backgroundImage: `url(${bgImage})`}}>
<nav className="landing-page-nav">
<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} />
<PrivacyButton setNavOpen={setNavOpen} togglePrivacy={togglePrivacy} isDropdown={true} />
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
</div>
</nav>
<div id="main-title">
<h1>{t("Lean Game Server")}</h1>
<p>
@@ -218,11 +184,8 @@ function LandingPage() {
</section>
<footer>
{/* Do not translate "Impressum", it's needed for German GDPR */}
<a className="link" onClick={openImpressum}>Impressum</a>
<a className="link" onClick={openPrivacy}>{t("Privacy Policy")}</a>
{privacyPopup? <PrivacyPolicyPopup handleClose={closePrivacy} />: null}
{impressumPopup? <ImpressumPopup handleClose={closeImpressum} />: null}
{preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
<a className="link" onClick={() => {setPopupContent("impressum")}}>Impressum</a>
<a className="link" onClick={() => {setPopupContent("privacy")}}>{t("Privacy Policy")}</a>
</footer>
</div>
+19 -23
View File
@@ -29,11 +29,10 @@ import Markdown from './markdown'
import {InventoryPanel} from './inventory'
import { hasInteractiveErrors } from './infoview/typewriter'
import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
ProofContext, SelectionContext, WorldLevelIdContext, PageContext } from './infoview/context'
import { DualEditor } from './infoview/main'
import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints'
import { ImpressumPopup, PrivacyPolicyPopup } from './popup/privacy_policy'
import path from 'path';
import '@fontsource/roboto/300.css'
@@ -43,7 +42,6 @@ import '@fontsource/roboto/700.css'
import 'lean4web/client/src/editor/infoview.css'
import 'lean4web/client/src/editor/vscode.css'
import '../css/level.css'
import { LevelAppBar } from './app_bar'
import { LeanClient } from 'lean4web/client/src/editor/leanclient'
import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader'
import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
@@ -61,10 +59,10 @@ monacoSetup()
function Level() {
const params = useParams()
const levelId = parseInt(params.levelId)
const worldId = params.worldId
// const levelId = parseInt(params.levelId)
// const worldId = params.worldId
const gameId = React.useContext(GameIdContext)
const {gameId, worldId, levelId} = React.useContext(GameIdContext)
// Load the namespace of the game
i18next.loadNamespaces(gameId).catch(err => {
@@ -87,14 +85,12 @@ function Level() {
function toggleInfo() {setInfo(!info)}
function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
useEffect(() => {}, [])
return <WorldLevelIdContext.Provider value={{worldId, levelId}}>
{levelId == 0 ?
<Introduction impressum={impressum} setImpressum={setImpressum} privacy={privacy} setPrivacy={setPrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup} /> :
<PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} privacy={privacy} setPrivacy={setPrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>}
{impressum ? <ImpressumPopup handleClose={closeImpressum} /> : null}
{privacy ? <PrivacyPolicyPopup handleClose={closePrivacy} /> : null}
{info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
{preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
</WorldLevelIdContext.Provider>
}
@@ -102,7 +98,7 @@ function ChatPanel({lastLevel, visible = true}) {
let { t } = useTranslation()
const chatRef = useRef<HTMLDivElement>(null)
const {mobile} = useContext(PreferencesContext)
const gameId = useContext(GameIdContext)
const {gameId} = useContext(GameIdContext)
const {worldId, levelId} = useContext(WorldLevelIdContext)
const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
const {proof, setProof} = useContext(ProofContext)
@@ -204,7 +200,7 @@ function ChatPanel({lastLevel, visible = true}) {
function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const {worldId, levelId} = useContext(WorldLevelIdContext)
const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
const gameInfo = useGetGameInfoQuery({game: gameId})
@@ -218,7 +214,7 @@ function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableR
function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo, togglePreferencesPopup}) {
let { t } = useTranslation()
const codeviewRef = useRef<HTMLDivElement>(null)
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const {worldId, levelId} = useContext(WorldLevelIdContext)
const {mobile} = React.useContext(PreferencesContext)
@@ -245,7 +241,7 @@ function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo
// A set of row numbers where help is displayed
const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
// Only for mobile layout
const [pageNumber, setPageNumber] = useState(0)
const {page, setPage} = useContext(PageContext)
// set to true to prevent switching between typewriter and editor
const [lockEditorMode, setLockEditorMode] = useState(false)
@@ -418,8 +414,8 @@ function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo
<ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
<EditorContext.Provider value={editorConnection}>
<MonacoEditorContext.Provider value={editor}>
<LevelAppBar
pageNumber={pageNumber} setPageNumber={setPageNumber}
{/* <LevelAppBar
pageNumber={page} setPageNumber={setPage}
isLoading={level.isLoading}
levelTitle={(mobile ? "" : t("Level")) + ` ${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
(level?.data?.title && ` : ${t(level?.data?.title, {ns: gameId})}`)}
@@ -427,15 +423,15 @@ function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo
togglePrivacy={togglePrivacy}
toggleInfo={toggleInfo}
togglePreferencesPopup={togglePreferencesPopup}
/>
/> */}
{mobile?
// TODO: This is copied from the `Split` component below...
<>
<div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
<ExercisePanel
codeviewRef={codeviewRef}
visible={pageNumber == 0} />
<InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
visible={page == 0} />
<InventoryPanel levelInfo={level?.data} visible={page == 1} />
</div>
</>
:
@@ -457,7 +453,7 @@ function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo
function IntroductionPanel({gameInfo}) {
let { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const {worldId} = useContext(WorldLevelIdContext)
const {mobile} = React.useContext(PreferencesContext)
@@ -487,7 +483,7 @@ export default Level
function Introduction({impressum, setImpressum, privacy, setPrivacy, toggleInfo, togglePreferencesPopup}) {
let { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const {mobile} = useContext(PreferencesContext)
const inventory = useLoadInventoryOverviewQuery({game: gameId})
@@ -506,7 +502,7 @@ function Introduction({impressum, setImpressum, privacy, setPrivacy, toggleInfo,
setPrivacy(!privacy)
}
return <>
<LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
{/* <LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/> */}
{gameInfo.isLoading ?
<div className="app-content loading"><CircularProgress /></div>
: mobile ?
@@ -552,7 +548,7 @@ function Introduction({impressum, setImpressum, privacy, setPrivacy, toggleInfo,
function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const {worldId, levelId} = useContext(WorldLevelIdContext)
const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
+276
View File
@@ -0,0 +1,276 @@
import * as React from 'react'
import { createContext, useContext, useState } from 'react'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
faArrowRight, faArrowLeft, faXmark, faBars, faCode,
faCircleInfo, faTerminal, faGear, IconDefinition, faShield } from '@fortawesome/free-solid-svg-icons'
import { GameIdContext } from "../app"
import { PageContext, PreferencesContext } from "./infoview/context"
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
import { downloadProgress } from './popup/erase'
import { useTranslation } from 'react-i18next'
import '../css/navigation.css'
import { PopupContext } from './popup/popup'
/** SVG github icon */
function GithubIcon () {
return <svg className="svg-inline--fa" height="24" aria-hidden="true" viewBox="0 0 16 16" version="1.1" width="24" >
<path fill="#fff" d="M8 0c4.42 0 8 3.58 8 8a8.013 8.013 0 0 1-5.45 7.59c-.4.08-.55-.17-.55-.38 0-.27.01-1.13.01-2.2 0-.75-.25-1.23-.54-1.48 1.78-.2 3.65-.88 3.65-3.95 0-.88-.31-1.59-.82-2.15.08-.2.36-1.02-.08-2.12 0 0-.67-.22-2.2.82-.64-.18-1.32-.27-2-.27-.68 0-1.36.09-2 .27-1.53-1.03-2.2-.82-2.2-.82-.44 1.1-.16 1.92-.08 2.12-.51.56-.82 1.28-.82 2.15 0 3.06 1.86 3.75 3.64 3.95-.23.2-.44.55-.51 1.07-.46.21-1.61.55-2.33-.66-.15-.24-.6-.83-1.23-.82-.67.01-.27.38.01.53.34.19.73.9.82 1.13.16.45.68 1.31 2.69.94 0 .67.01 1.3.01 1.49 0 .21-.15.45-.55.38A7.995 7.995 0 0 1 0 8c0-4.42 3.58-8 8-8Z"></path>
</svg>
}
/** A button to appear in the navigation (both, top bar or dropdown). */
export const NavButton: React.FC<{
icon?: IconDefinition
iconElement?: JSX.Element
text?: string
onClick?: React.MouseEventHandler<HTMLAnchorElement>
title?: string
href?: string
inverted?: boolean
disabled?: boolean
}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false}) => {
return <a className={`nav-button btn${inverted?' btn-inverted':''}${disabled?' btn-disabled':''}`} onClick={disabled?null:onClick} href={disabled?null:href} title={title}>
{iconElement ?? (icon && <FontAwesomeIcon icon={icon} />)}{text && <>&nbsp;{text}</>}
</a>
}
/** Context which manages the dropdown navigation */
const NavigationContext = createContext<{
navOpen: boolean,
setNavOpen: React.Dispatch<React.SetStateAction<boolean>>
}>({navOpen: false, setNavOpen: () => {}})
/** Content of the navigation on Desktop during world selection. */
function DesktopNavigationOverview () {
const { t } = useTranslation()
const {gameId} = useContext(GameIdContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
return <div className="nav-content">
<div className="nav-title-left"></div>
<div className="nav-title-middle">
<span className="nav-title">{t(gameInfo.data?.title, {ns: gameId})}</span>
</div>
<div className="nav-title-right"></div>
</div>
}
/** Content of the navigation on Mobile during world selection. */
function MobileNavigationOverview () {
const { t } = useTranslation()
const {page, setPage} = useContext(PageContext)
return <div className="nav-content">
<div className="nav-title-left"></div>
<div className="nav-title-middle">
<span className="nav-title">
</span>
</div>
<div className="nav-title-right">
{page > 0 &&
<NavButton
text={page == 1 ? t("Intro") : null}
icon={page == 1 ? null : faBookOpen}
onClick={() => setPage(page - 1)}
inverted={true} />
}
{ page < 2 &&
<NavButton
text={(page==0) ? t("Start") : null}
icon={(page==0) ? null : faBook}
onClick={() => setPage(page+1)}
inverted={true} />
}
</div>
</div>
}
/** Content of the navigation during game selection. */
function NavigationLandingPage () {
return <div className="nav-content">
<div className="nav-title-left"></div>
<div className="nav-title-middle"></div>
<div className="nav-title-right"></div>
</div>
}
/** Content of the navigation on Desktop in a level. */
function DesktopNavigationLevel () {
const { t } = useTranslation()
const { gameId, worldId, levelId } = useContext(GameIdContext)
const { typewriterMode, setTypewriterMode, lockEditorMode } = useContext(PageContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
/** toggle input mode if allowed */
function toggleInputMode(ev: React.MouseEvent) {
if (!lockEditorMode) {
setTypewriterMode(!typewriterMode)
console.log('test')
}
}
const worldTitle = gameInfo.data?.worlds.nodes[worldId]?.title
const levelTitle = ((levelId == 0) ?
t("Introduction") :
(
t("Level") +
` ${levelId}` +
(gameInfo.data?.worldSize[worldId] ? ` / ${gameInfo.data?.worldSize[worldId]}` : '') +
(levelInfo.data?.title ? ` : ${t(levelInfo?.data?.title, {ns: gameId})}` : '')
)
)
return <div className="nav-content">
<div className="nav-title-left">
<span className="nav-title">{worldTitle ? `${t("World")}: ${t(worldTitle, {ns: gameId})}` : ''}
</span>
</div>
<div className="nav-title-middle">
<span className="nav-title">
{ levelTitle
}
</span>
</div>
<div className="nav-title-right" >
{ levelId > 0 &&
<NavButton
icon={faArrowLeft}
text={t("Previous")}
inverted={true}
href={`#/${gameId}/world/${worldId}/level/${levelId - 1}`} />
}
{ levelId == gameInfo.data?.worldSize[worldId] ?
<NavButton
icon={faHome}
text={t("Leave World")}
inverted={true}
href={`#/${gameId}`} /> :
<NavButton
icon={faArrowRight}
text={levelId == 0 ? t("Start") : t("Next")} inverted={true}
href={`#/${gameId}/world/${worldId}/level/${levelId + 1}`} />
}
{ levelId > 0 &&
<NavButton
icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal}
inverted={true}
disabled={levelId == 0 || lockEditorMode}
onClick={(ev) => toggleInputMode(ev)}
title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} />
}
</div>
</div>
}
/** Content of the navigation on Mobile in a level. */
function MobileNavigationLevel () {
const { t } = useTranslation()
const {gameId, worldId, levelId} = useContext(GameIdContext)
const {page, setPage} = useContext(PageContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
let title = worldId ?
` ${levelId} / ${gameInfo.data?.worldSize[worldId]}`+ (levelInfo?.data?.title && ` : ${t(levelInfo?.data?.title, {ns: gameId})}`)
:
''
return <div className="nav-content">
<div className="nav-title-left"></div>
<div className="nav-title-middle">
<span className="nav-title">
{title}
</span>
</div>
<div className="nav-title-right">
<NavButton
icon={page?faBookOpen:faBook}
onClick={() => setPage(page?0:1)}
inverted={true}/>
</div>
</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 { setPopupContent } = useContext(PopupContext)
const [navOpen, setNavOpen] = useState(false)
function toggleNav () {setNavOpen(!navOpen)}
return <nav>
<NavigationContext.Provider value={{navOpen, setNavOpen}}>
{ gameId && <>
<NavButton
icon={worldId ? faHome : faGlobe}
title={worldId ? t("back to world selection") : t("back to games selection")}
href={worldId ? `#/${gameId}` : `#`} />
</>}
{ gameId ?
worldId ?
(mobile ? <MobileNavigationLevel /> : <DesktopNavigationLevel />) :
(mobile ? <MobileNavigationOverview /> : <DesktopNavigationOverview />) :
<NavigationLandingPage />
}
{ !gameId &&
<NavButton
iconElement={<GithubIcon />}
title={t("view the Lean game server on Github")}
href='https://github.com/leanprover-community/lean4game'
/>
}
<NavButton
icon={navOpen ? faXmark : faBars}
title={navOpen ? t('close menu') : t('open menu')}
onClick={toggleNav} />
{ navOpen &&
<div className='dropdown' onClick={toggleNav} >
{ gameId && <>
<NavButton
icon={faCircleInfo}
text={t("Game Info")}
onClick={() => {setPopupContent("info")}}
inverted={true} />
<NavButton
icon={faEraser}
text={t("Erase")}
onClick={() => {setPopupContent("erase")}}
inverted={true} />
<NavButton
icon={faDownload}
text={t("Download")}
onClick={() => {downloadProgress(gameId)}}
inverted={true} />
<NavButton
icon={faUpload}
text={t("Upload")}
onClick={() => {setPopupContent("upload")}}
inverted={true} />
</>}
<NavButton
icon={faCircleInfo}
text={"Impressum"}
onClick={() => {setPopupContent("impressum")}}
inverted={true} />
<NavButton
icon={faShield}
text={t("Privacy Policy")}
onClick={() => {setPopupContent("privacy")}}
inverted={true} />
<NavButton
icon={faGear}
text={t("Preferences")}
onClick={() => {setPopupContent("preferences")}}
inverted={true} />
</div>
}
</NavigationContext.Provider>
</nav>
}
+14 -16
View File
@@ -1,6 +1,3 @@
/**
* @fileOverview
*/
import * as React from 'react'
import { useSelector } from 'react-redux'
import { GameIdContext } from '../../app'
@@ -9,10 +6,14 @@ import { deleteProgress, selectProgress } from '../../state/progress'
import { downloadFile } from '../world_tree'
import { Button } from '../button'
import { Trans, useTranslation } from 'react-i18next'
import { useContext } from 'react'
import { PopupContext } from './popup'
/** download the current progress (i.e. what's saved in the browser store) */
export function downloadProgress(gameId: string, gameProgress: any, ev: React.MouseEvent) {
ev.preventDefault()
export function downloadProgress(gameId: string) {
const gameProgress = useSelector(selectProgress(gameId))
// ev.preventDefault()
downloadFile({
data: JSON.stringify(gameProgress, null, 2),
fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
@@ -25,26 +26,24 @@ export function downloadProgress(gameId: string, gameProgress: any, ev: React.Mo
* `handleClose` is the function to close it again because it's open/closed state is
* controlled by the containing element.
*/
export function ErasePopup ({handleClose}) {
export function ErasePopup () {
let { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const gameProgress = useSelector(selectProgress(gameId))
const dispatch = useAppDispatch()
const { setPopupContent } = useContext(PopupContext)
const eraseProgress = () => {
dispatch(deleteProgress({game: gameId}))
handleClose()
setPopupContent(null)
}
const downloadAndErase = (ev) => {
downloadProgress(gameId, gameProgress, ev)
downloadProgress(gameId)
eraseProgress()
}
return <div className="modal-wrapper">
<div className="modal-backdrop" onClick={handleClose} />
<div className="modal">
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
return <>
<h2>{t("Delete Progress?")}</h2>
<Trans>
<p>Do you want to delete your saved progress irreversibly?</p>
@@ -55,7 +54,6 @@ export function ErasePopup ({handleClose}) {
</Trans>
<Button onClick={eraseProgress} to="">{t("Delete")}</Button>
<Button onClick={downloadAndErase} to="">{t("Download & Delete")}</Button>
<Button onClick={handleClose} to="">{t("Cancel")}</Button>
</div>
</div>
<Button onClick={() => {setPopupContent(null)}} to="">{t("Cancel")}</Button>
</>
}
+7 -9
View File
@@ -6,22 +6,21 @@ import { Typography } from '@mui/material'
import Markdown from '../markdown'
import { Trans, useTranslation } from 'react-i18next'
import { GameIdContext } from '../../app'
import { useGetGameInfoQuery } from '../../state/api'
/** Pop-up that is displaying the Game Info.
*
* `handleClose` is the function to close it again because it's open/closed state is
* controlled by the containing element.
*/
export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
export function InfoPopup () {
let { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
return <div className="modal-wrapper">
<div className="modal-backdrop" onClick={handleClose} />
<div className="modal">
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
return <>
<Typography variant="body1" component="div" className="welcome-text">
<Markdown>{t(info, {ns: gameId})}</Markdown>
<Markdown>{t(gameInfo.data?.info, {ns: gameId})}</Markdown>
<hr />
<Trans>
<h2>Progress saving</h2>
@@ -51,6 +50,5 @@ export function InfoPopup ({info, handleClose}: {info: string, handleClose: () =
</p>
</Trans>
</Typography>
</div>
</div>
</>
}
+43
View File
@@ -0,0 +1,43 @@
import * as React from 'react'
import { Trans, useTranslation } from 'react-i18next';
/** Pop-up that is displayed when opening the privacy policy. */
export function ImpressumPopup () {
let {t, i18n} = useTranslation()
function content (lng = i18n.language) {
const tt = i18n.getFixedT(lng);
return <Trans t={tt} >
<h2>Impressum</h2>
<p>
<strong>Contact:</strong><br />
Marcus Zibrowius, Jon Eugster<br />
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
Universitätsstr. 1<br />
40225 Düsseldorf<br />
Germany<br />
+49 211 81-14690<br />
<a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team">Contact Details</a>
</p>
<p>
<strong>Legal form:</strong><br />
The Heinrich Heine University Düsseldorf is a corporation under public law. It is legally represented by the Rector Prof. Dr. Anja Steinbeck. The responsible supervisory authority is the Ministry of Culture and Science of North Rhine-Westphalia, Völklinger Straße 49, 40221 Düsseldorf.
</p>
<p>
<strong>VAT identification number:</strong><br />
according to §27a Sales Tax Act<br />
DE 811222416
</p>
<p><a href="https://www.hhu.de/impressum" target="_blank">Impressum HHU</a></p>
</Trans>
}
return <>
{i18n.language != 'en' && <>
<p><i>(English version below)</i></p>
{content()}
<hr />
</>}
{content('en')}
</>
}
+50
View File
@@ -0,0 +1,50 @@
import * as React from 'react'
import { useContext } from 'react'
import { PrivacyPolicyPopup } from './privacy_policy'
import { ImpressumPopup } from './impressum'
import { InfoPopup } from './game_info'
import { ErasePopup } from './erase'
import { PreferencesPopup } from './preferences'
import { UploadPopup } from './upload'
/** The context which manages if a popup is shown.
* If `popupContent` is `null`, the popup is closed.
*/
export const PopupContext = React.createContext<{
popupContent: string,
setPopupContent: React.Dispatch<React.SetStateAction<string>>
}>({
popupContent: null,
setPopupContent: () => {}
})
/** To create a new Popup, one needs to add its content as `React.JSX.Element` here
* and then call `setPopupConent(key)` at the place where to popup should be opened.
*
* TODO: The drawback of this design is that there is no check for key missmatches.
* How could that be achieved?
*/
export const Popups = {
"erase": <ErasePopup />,
"impressum": <ImpressumPopup />,
"info": <InfoPopup />,
"preferences": <PreferencesPopup />,
"privacy": <PrivacyPolicyPopup />,
"upload": <UploadPopup />,
}
/** The skeleton for the popups. */
export function Popup () {
const {popupContent, setPopupContent} = useContext(PopupContext)
function closePopup() {
setPopupContent(null)
}
return <div className="modal-wrapper">
<div className="modal-backdrop" onClick={closePopup} />
<div className="modal">
<div className="codicon codicon-close modal-close" onClick={closePopup}></div>
{Popups[popupContent]}
</div>
</div>
}
+3 -8
View File
@@ -12,12 +12,11 @@ import { IPreferencesContext, PreferencesContext } from "../infoview/context"
import ReactCountryFlag from 'react-country-flag';
import { useTranslation } from 'react-i18next';
export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
export function PreferencesPopup () {
let { t } = useTranslation()
const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
const marks = [
{
value: 0,
@@ -44,10 +43,7 @@ export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
setLanguage(ev.target.value as IPreferencesContext["language"])
}
return <div className="modal-wrapper">
<div className="modal-backdrop" onClick={handleClose} />
<div className="modal">
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
return <>
<Typography variant="body1" component="div" className="settings">
<div className='preferences-category'>
<div className='category-title'>
@@ -118,6 +114,5 @@ export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
</div>
</div>
</Typography>
</div>
</div>
</>
}
+9 -73
View File
@@ -1,19 +1,11 @@
/**
* @fileOverview The impressum/privacy policy
*/
import { faShield } from '@fortawesome/free-solid-svg-icons';
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome';
import * as React from 'react'
import { Trans, useTranslation } from 'react-i18next';
/** Pop-up that is displayed when opening the privacy policy.
*
* `handleClose` is the function to close it again because it's open/closed state is
* controlled by the containing element.
*
* Note: Do not translate the Impressum!
*/
export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
export function PrivacyPolicyPopup () {
let {t, i18n} = useTranslation()
function content (lng = i18n.language) {
const tt = i18n.getFixedT(lng);
@@ -45,68 +37,12 @@ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
</Trans>
}
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>
{i18n.language != 'en' && <>
<p><i>(English version below)</i></p>
{content()}
<hr />
</>}
{content('en')}
</div>
</div>
}
/** Pop-up that is displayed when opening the privacy policy.
*
* `handleClose` is the function to close it again because it's open/closed state is
* controlled by the containing element.
*
* Note: Do not translate the Impressum!
*/
export function ImpressumPopup ({handleClose}: {handleClose: () => void}) {
let {t, i18n} = useTranslation()
function content (lng = i18n.language) {
const tt = i18n.getFixedT(lng);
return <Trans t={tt} >
<h2>Impressum</h2>
<p>
<strong>Contact:</strong><br />
Marcus Zibrowius, Jon Eugster<br />
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
Universitätsstr. 1<br />
40225 Düsseldorf<br />
Germany<br />
+49 211 81-14690<br />
<a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team">Contact Details</a>
</p>
<p>
<strong>Legal form:</strong><br />
The Heinrich Heine University Düsseldorf is a corporation under public law. It is legally represented by the Rector Prof. Dr. Anja Steinbeck. The responsible supervisory authority is the Ministry of Culture and Science of North Rhine-Westphalia, Völklinger Straße 49, 40221 Düsseldorf.
</p>
<p>
<strong>VAT identification number:</strong><br />
according to §27a Sales Tax Act<br />
DE 811222416
</p>
<p><a href="https://www.hhu.de/impressum" target="_blank">Impressum HHU</a></p>
</Trans>
}
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>
{i18n.language != 'en' && <>
<p><i>(English version below)</i></p>
{content()}
<hr />
</>}
{content('en')}
</div>
</div>
return <>
{i18n.language != 'en' && <>
<p><i>(English version below)</i></p>
{content()}
<hr />
</>}
{content('en')}
</>
}
+9 -9
View File
@@ -9,20 +9,24 @@ import { GameProgressState, loadProgress, selectProgress } from '../../state/pro
import { downloadFile } from '../world_tree'
import { Button } from '../button'
import { Trans, useTranslation } from 'react-i18next'
import { PopupContext } from './popup'
import { useContext } from 'react'
/** Pop-up that is displaying the Game Info.
*
* `handleClose` is the function to close it again because it's open/closed state is
* controlled by the containing element.
*/
export function UploadPopup ({handleClose}) {
export function UploadPopup () {
let { t } = useTranslation()
const [file, setFile] = React.useState<File>();
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const gameProgress = useSelector(selectProgress(gameId))
const dispatch = useAppDispatch()
const { setPopupContent } = useContext(PopupContext)
const handleFileChange = (e) => {
if (e.target.files) {
setFile(e.target.files[0])
@@ -39,7 +43,7 @@ export function UploadPopup ({handleClose}) {
console.debug("Json Data", data)
dispatch(loadProgress({game: gameId, data: data}))
}
handleClose()
setPopupContent(null) // close the popup
}
/** Download the current progress (i.e. what's saved in the browser store) */
@@ -53,10 +57,7 @@ export function UploadPopup ({handleClose}) {
}
return <div className="modal-wrapper">
<div className="modal-backdrop" onClick={handleClose} />
<div className="modal">
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
return <>
<h2>{t("Upload Saved Progress")}</h2>
<Trans>
<p>Select a JSON file with the saved game progress to load your progress.</p>
@@ -70,6 +71,5 @@ export function UploadPopup ({handleClose}) {
</p>
<Button to="" onClick={uploadProgress}>{t("Load selected file")}</Button>
</div>
</div>
</>
}
+16 -19
View File
@@ -10,18 +10,17 @@ import { useAppDispatch, useAppSelector } from '../hooks'
import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
import { Button } from './button'
import { PreferencesContext } from './infoview/context'
import { PageContext, PreferencesContext } from './infoview/context'
import { InventoryPanel } from './inventory'
import { ErasePopup } from './popup/erase'
import { InfoPopup } from './popup/game_info'
import { ImpressumPopup, PrivacyPolicyPopup } from './popup/privacy_policy'
import { PrivacyPolicyPopup } from './popup/privacy_policy'
import { RulesHelpPopup } from './popup/rules_help'
import { UploadPopup } from './popup/upload'
import { PreferencesPopup} from "./popup/preferences"
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'
@@ -30,7 +29,7 @@ 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)
const {gameId} = React.useContext(GameIdContext)
let { t } = useTranslation()
@@ -68,7 +67,7 @@ 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)
const {gameId} = React.useContext(GameIdContext)
// Load the namespace of the game
i18next.loadNamespaces(gameId)
@@ -81,7 +80,12 @@ function Welcome() {
// For mobile only
const openedIntro = useAppSelector(selectOpenedIntro(gameId))
const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
const {page, setPage} = React.useContext(PageContext)
// TODO: recover `openedIntro` functionality
// const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
// pop-ups
const [eraseMenu, setEraseMenu] = React.useState(false)
@@ -118,15 +122,15 @@ function Welcome() {
<CircularProgress />
</Box>
: <>
<WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy}
{/* <WelcomeAppBar pageNumber={page} setPageNumber={setPage} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy}
toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/> */}
<div className="app-content">
{ mobile ?
<div className="welcome mobile">
{(pageNumber == 0 ?
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
: pageNumber == 1 ?
{(page == 0 ?
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPage} />
: page == 1 ?
<WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
:
@@ -135,20 +139,13 @@ function Welcome() {
</div>
:
<Split className="welcome" minSize={0} snapOffset={200} sizes={[25, 50, 25]}>
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPage} />
<WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
<InventoryPanel levelInfo={inventory?.data} />
</Split>
}
</div>
{impressum ? <ImpressumPopup handleClose={closeImpressum} /> : null}
{privacy ? <PrivacyPolicyPopup handleClose={closePrivacy} /> : null}
{rulesHelp ? <RulesHelpPopup handleClose={closeRulesHelp} /> : null}
{eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
{uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
{info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
{preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
</>
}
+4 -4
View File
@@ -65,7 +65,7 @@ export function LevelIcon({ world, level, position, completed, unlocked, worldSi
// Sinus-Satz: (1.1*r) / sin(β/2) = R / sin(π/2)
let R = 1.1 * r / Math.sin(beta/2)
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const difficulty = useSelector(selectDifficulty(gameId))
const levelDisabled = (difficulty >= 2 && !(unlocked || completed))
@@ -137,7 +137,7 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
nextLevel = 0
}
let playable = difficulty <= 1 || completed || unlocked
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
return <Link
to={playable ? `/${gameId}/world/${world}/level/${nextLevel}` : ''}
@@ -198,7 +198,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 {gameId} = React.useContext(GameIdContext)
const difficulty = useSelector(selectDifficulty(gameId))
const dispatch = useAppDispatch()
const { mobile } = React.useContext(PreferencesContext)
@@ -277,7 +277,7 @@ export function WorldTreePanel({worlds, worldSize, rulesHelp, setRulesHelp}:
rulesHelp: boolean,
setRulesHelp: any,
}) {
const gameId = React.useContext(GameIdContext)
const {gameId} = React.useContext(GameIdContext)
const difficulty = useSelector(selectDifficulty(gameId))
const {nodes, bounds}: any = worlds ? computeWorldLayout(worlds) : {nodes: []}
+18 -3
View File
@@ -6,14 +6,13 @@
--clr-light-gray: #ddd;
--clr-dark-gray: #aaa;
--clr-darker-gray: #555;
--ff-primary: Roboto;
}
/* General styling */
body {
font-family: var(--ff-primary);
font-family: "Roboto", sans-serif;
-webkit-font-smoothing: antialiased;
-moz-osx-font-smoothing: grayscale;
}
@@ -98,6 +97,7 @@ em {
flex-direction: column;
}
/* TODO: remove */
.app-bar {
flex: 0;
background: var(--clr-primary);
@@ -142,7 +142,7 @@ em {
margin:0 1.5em 1.5em 1.5em;
}
.privacy-policy {
.modal-wrapper {
z-index: 10;
}
@@ -151,3 +151,18 @@ em {
margin-bottom: 3rem;
border-color: var(--vscode-breadcrumb-foreground);
}
/* TODO: should not be #root */
#root code {
font-family: "JuliaMono", monospace;
}
@font-face {
font-family: 'JuliaMono';
src: local('JuliaMono'), url('/fonts/JuliaMono-Regular.ttf') format('truetype');
}
@font-face {
font-family: 'Roboto';
src: local('Roboto'), url('/fonts/Roboto-Regular.ttf') format('truetype');
}
+2 -6
View File
@@ -9,10 +9,6 @@ html {
font-size: 16px;
}
body {
font-family: system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, "Noto Sans", "Liberation Sans", sans-serif, "Apple Color Emoji", "Segoe UI Emoji", "Segoe UI Symbol", "Noto Color Emoji";
}
a {
text-decoration: none;
}
@@ -165,12 +161,12 @@ header {
font-style: italic;
}
header nav {
/* header nav {
display: flex;
justify-content: flex-end;
padding: 8px;
background-color: rgba(0, 133, 162, .7);
}
} */
footer {
background-color: rgba(0, 133, 162, 1);
+77
View File
@@ -0,0 +1,77 @@
nav {
flex: 0;
background: var(--clr-primary);
display: flex;
position: relative;
flex-direction: row;
justify-content: space-between;
align-items: center;
padding: 1.1em;
filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
z-index: 2;
}
.nav-content {
flex: 1;
display: flex;
}
.nav-content > div {
/* border: 1px solid red; */
text-align: center;
}
.nav-title-left, .nav-title-right {
flex-grow: 0;
flex-shrink: 0;
display: flex;
align-items: center;
}
.nav-title-middle {
flex-grow: 1;
flex-shrink: 1;
margin-left: .5rem;
margin-right: .5rem;
}
.nav-title {
color: white;
font-weight: 500;
font-size: 1.3rem;
display: inline-block;
margin: 0;
/* margin: 0 1em; */
}
/* fix to make toggle buttons work */
.svg-inline--fa {
width: 1em;
}
/* TODO */
.nav-button:not(.btn-inverted) {
font-size: 1.3rem;
}
.dropdown {
z-index: 10;
}
.dropdown {
position: absolute;
display: flex;
flex-direction: column;
right: 0;
top: 100%;
background-color: #fff;
z-index: 5;
border-top: 1px solid rgba(0, 0, 0, 0.1);
border-bottom: 1px solid rgba(0, 0, 0, 0.1);
box-shadow: -.1rem .3rem .3rem 0 rgba(0, 0, 0, 0.1);
}
.dropdown .svg-inline--fa {
width: 1.8rem;
}
+15 -16
View File
@@ -16,23 +16,21 @@ import './i18n';
// If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
// `/g/local/game`. This is used for the devcontainer setup
let single_game = (import.meta.env.VITE_LEAN4GAME_SINGLE == "true")
let root_object: RouteObject = single_game ? {
path: "/",
loader: () => redirect("/g/local/game")
} : {
path: "/",
element: <App />,
errorElement: <ErrorPage />,
children: [
{
path: "/",
element: <LandingPage />,
}
]
}
// let root_object: RouteObject = single_game ? {
// path: "/",
// loader: () => redirect("/g/local/game")
// }
let landing_page: RouteObject = single_game ? {
path: "/",
loader: () => redirect("/g/local/game")
} : {
path: "/",
element: <LandingPage />,
}
const router = createHashRouter([
root_object,
// root_object,
{
// For backwards compatibility
path: "/game/nng",
@@ -44,10 +42,11 @@ const router = createHashRouter([
loader: () => redirect("/g/leanprover-community/NNG4")
},
{
path: "/g/:owner/:repo",
path: "/",
element: <App />,
errorElement: <ErrorPage />,
children: [
landing_page,
{
path: "/g/:owner/:repo",
element: <Welcome />,
+1 -1
View File
@@ -205,7 +205,7 @@ export function selectOpenedIntro(game: string) {
/** return typewriter mode for the current game if it exists */
export function selectTypewriterMode(game: string) {
return (state) => {
return state.progress.games[game.toLowerCase()]?.typewriterMode ?? true
return state.progress.games[game?.toLowerCase()]?.typewriterMode ?? true
}
}