diff --git a/client/src/app.tsx b/client/src/app.tsx index d037446..9c15c84 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -49,10 +49,18 @@ function App() { // mobile only: game intro should only be shown once and skipped afterwards useEffect(() => { - if (openedIntro && !worldId && page == 0) { + if (worldId) { + console.log('setting page to 1') setPage(1) + } else { + if (openedIntro && page == 0) { + console.log('setting page to 1') + setPage(1) + } else { + // setPage(0) + } } - }, [openedIntro]) + }, [openedIntro, worldId, levelId]) // option to pass language as `?lang=de` in the URL useEffect(() => { @@ -96,11 +104,9 @@ function App() { - - - + + { popupContent && } - { popupContent && } diff --git a/client/src/components/chat.tsx b/client/src/components/chat.tsx new file mode 100644 index 0000000..4ce6602 --- /dev/null +++ b/client/src/components/chat.tsx @@ -0,0 +1,104 @@ +import * as React from 'react' +import { PageContext, PreferencesContext } from './infoview/context' +import { GameIdContext } from '../app' +import { useTranslation } from 'react-i18next' +import { useAppDispatch } from '../hooks' +import { Hint } from './hints' +import { Button } from './button' +import { changedOpenedIntro } from '../state/progress' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faArrowRight } from '@fortawesome/free-solid-svg-icons' +import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api' +import { useContext, useEffect, useRef, useState } from 'react' +import '../css/level.css' +import '../css/chat.css' + +/** Split a string by double newlines and filters out empty segments. */ +function splitIntro (intro : string) { + return intro.split(/\n(\s*\n)+/).filter(t => t.trim()) +} + +/** The buttons at the bottom of chat */ +export function ChatButtons () { + + const { gameId, worldId, levelId } = useContext(GameIdContext) + const {setPage} = useContext(PageContext) + const dispatch = useAppDispatch() + const gameInfo = useGetGameInfoQuery({game: gameId}) + + return
+ {(!worldId || !levelId) && + // Start button appears only on world selection and level 0. + + } +
+} + +/** the panel showing the game's introduction text */ +export function ChatPanel ({visible = true}) { + + let { t } = useTranslation() + const chatRef = useRef(null) + + const { mobile } = useContext(PreferencesContext) + const { gameId, worldId, levelId } = useContext(GameIdContext) + + const gameInfo = useGetGameInfoQuery({game: gameId}) + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + + let [chatMessages, setChatMessages] = useState>([]) + + // Effect to clear chat and display the correct intro text + useEffect(() => { + if (levelId > 0) { + // playable level: show the level's intro + if (levelInfo.data?.introduction) { + setChatMessages([t(levelInfo.data?.introduction, {ns : gameId})]) + } + else { + setChatMessages([]) + } + } else { + if (worldId) { + // Level 0: show the world's intro + if (gameInfo.data?.worlds.nodes[worldId].introduction) { + setChatMessages(splitIntro(t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}))) + } else { + setChatMessages([]) + } + } else { + // world overview: show the game's intro + if (gameInfo.data?.introduction) { + setChatMessages(splitIntro(t(gameInfo.data?.introduction, {ns : gameId}))) + } else { + setChatMessages([]) + } + } + } + }, [gameInfo, levelInfo, gameId, worldId, levelId]) + + return
+
+ + {chatMessages.map(((t, i) => + t.trim() ? + + : <> + ))} +
+ { mobile && } +
+} diff --git a/client/src/components/game.tsx b/client/src/components/game.tsx index 32366f0..45a2b31 100644 --- a/client/src/components/game.tsx +++ b/client/src/components/game.tsx @@ -1,16 +1,101 @@ -import i18next from "i18next" -import React from "react" -import { useParams } from "react-router-dom" -import { GameIdContext } from "../app" -import { useGetGameInfoQuery } from "../state/api" +import * as React from 'react' +import { useEffect, useRef } from 'react' +import Split from 'react-split' +import { Box, CircularProgress } from '@mui/material' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faArrowRight } from '@fortawesome/free-solid-svg-icons' +import { GameIdContext } from '../app' +import { useAppDispatch, useAppSelector } from '../hooks' +import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' +import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' +import { Button } from './button' +import { PageContext, PreferencesContext } from './infoview/context' +import { InventoryPanel } from './inventory' +import { ErasePopup } from './popup/erase' +import { InfoPopup } from './popup/info' +import { PrivacyPolicyPopup } from './popup/privacy' +import { UploadPopup } from './popup/upload' +import { PreferencesPopup} from "./popup/preferences" +import { WorldTreePanel } from './world_tree' + +import '../css/game.css' +import '../css/welcome.css' +import '../css/level.css' +import { Hint } from './hints' +import i18next from 'i18next' +import { useTranslation } from 'react-i18next' +import { LoadingIcon } from './utils' +import { ChatPanel } from './chat' +import { DualEditor } from './infoview/main' +import { Level } from './level' + +/** main page of the game showing among others the tree of worlds/levels */ function Game() { - const params = useParams() - const levelId = parseInt(params.levelId) - const worldId = params.worldId - return
- + const codeviewRef = useRef(null) + + const { gameId, worldId, levelId } = React.useContext(GameIdContext) + + // Load the namespace of the game + i18next.loadNamespaces(gameId) + + const {mobile} = React.useContext(PreferencesContext) + const {isSavePreferences, language, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext) + + const gameInfo = useGetGameInfoQuery({game: gameId}) + const inventory = useLoadInventoryOverviewQuery({game: gameId}) + + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + + + 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) + const [impressum, setImpressum] = React.useState(false) + const [privacy, setPrivacy] = React.useState(false) + const [info, setInfo] = React.useState(false) + const [rulesHelp, setRulesHelp] = React.useState(false) + const [uploadMenu, setUploadMenu] = React.useState(false) + const [preferencesPopup, setPreferencesPopup] = React.useState(false) + + // set the window title + useEffect(() => { + if (gameInfo.data?.title) { + window.document.title = gameInfo.data.title + } + }, [gameInfo.data?.title]) + + return mobile ? +
+ {<> + + { worldId ? + 0 && page == 1} /> : + + } + + + } +
+ : + + +
+ {/* Note: apparently without this `div` the split panel bugs out. */} + {worldId ? : } +
+ + + +} -
+export default Game +function useLevelEditor(codeviewRef: React.MutableRefObject, initialCode: any, initialSelections: any, onDidChangeContent: any, onDidChangeSelection: any): { editor: any; infoProvider: any; editorConnection: any } { + throw new Error('Function not implemented.') } diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index ab072d9..5d1bc79 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -536,7 +536,7 @@ export function TypewriterInterface({props}) { [DiagnosticSeverity.Hint]: 'hint', }[diag.severity] : ''; - return
+ return

{t("Line")} {diag.range.start.line}, {t("Character")} {diag.range.start.character}

diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
index 964752d..77cc599 100644
--- a/client/src/components/inventory.tsx
+++ b/client/src/components/inventory.tsx
@@ -1,92 +1,122 @@
-import * as React from 'react';
-import { useState, useEffect } from 'react';
+import * as React from 'react'
+import { useState, useEffect, createContext, useContext } from 'react';
 import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
+import { faLock, faBan, faCheck, faXmark } from '@fortawesome/free-solid-svg-icons'
 import { faClipboard } from '@fortawesome/free-regular-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
-import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
+import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api';
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
 import { useTranslation } from 'react-i18next';
 import { t } from 'i18next';
 import { WorldLevelIdContext } from './infoview/context';
+import { NavButton } from './navigation';
+import { LoadingIcon } from './utils';
+
+
+/** Context which manages the inventory */
+const InventoryContext = createContext<{
+  theoremTab: string,
+  setTheoremTab: React.Dispatch>,
+  categoryTab: "tactic"|"theorem"|"definition",
+  setCategoryTab: React.Dispatch>,
+  docTile: any,
+  setDocTile: React.Dispatch>
+}>({
+  theoremTab: null,
+  setTheoremTab: () => {},
+  categoryTab: "tactic",
+  setCategoryTab: () => {},
+  docTile: null,
+  setDocTile: () => {}
+})
+
+
+/**
+ */
+function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false }) {
+  const icon = locked ?  :
+               disabled ?  : item.st
+  const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
+  // Note: This is somewhat a hack as the statement of lemmas comes currently in the form
+  // `Namespace.statement_name (x y : Nat) : some type`
+  const title = locked ? t("Not unlocked yet") :
+                disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
 
-export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
-  {
-    levelInfo: LevelInfo|InventoryOverview,
-    openDoc: (props: {name: string, type: string}) => void,
-    lemmaTab: any,
-    setLemmaTab: any,
-    enableAll?: boolean,
-  }) {
-  const { t } = useTranslation()
+  const { gameId } = React.useContext(GameIdContext)
+  const difficulty = useSelector(selectDifficulty(gameId))
 
-  // TODO: this state should be preserved when loading a different level.
-  const [tab, setTab] = useState<"tactic"|"theorem"|"definition">("theorem")
+  // local state to show checkmark after pressing the copy button
+  const [copied, setCopied] = useState(false)
 
-  let newTheorems = levelInfo?.lemmas?.filter(item => item.new).length > 0
-  let newTactics = levelInfo?.tactics?.filter(item => item.new).length > 0
-  let newDefinitions = levelInfo?.definitions?.filter(item => item.new).length > 0
+  const handleClick = () => {
+    // if ((difficulty == 0) || !locked) {
+      showDoc()
+    // }
+  }
 
-  return (
-    

-      

-        
 { setTab("theorem") }}>{t("Theorems")}

-        
 { setTab("tactic") }}>{t("Tactics")}

-        
 { setTab("definition") }}>{t("Definitions")}

-      

-      { (tab == "theorem") && levelInfo?.lemmas &&
-        
-      }
-      { (tab == "tactic") && levelInfo?.tactics &&
-        
-      }
-      { (tab == "definition") && levelInfo?.definitions &&
-        
-      }
+  const copyItemName = (ev) => {
+    navigator.clipboard.writeText(displayName)
+    setCopied(true)
+    setInterval(() => {
+      setCopied(false)
+    }, 3000);
+    ev.stopPropagation()
+  }
+
+  return 

+    {icon} {displayName}
+    

+      {copied ?  : }
     

-  )
+  

 }
 
-function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} :
+
+function InventoryList({ items, tab=null, setTab=()=>{} } :
   {
     items: InventoryTile[],
-    docType: string,
-    openDoc(props: {name: string, type: string}): void,
-    tab?: any,
-    setTab?: any,
-    level?: LevelInfo|InventoryOverview,
-    enableAll?: boolean,
+    tab?: string,
+    setTab?: React.Dispatch>
   }) {
-  // 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 {worldId, levelId} = React.useContext(WorldLevelIdContext)
+  const { gameId, worldId, levelId } = React.useContext(GameIdContext)
+  const { setDocTile, categoryTab, setCategoryTab } = useContext(InventoryContext)
 
   const difficulty = useSelector(selectDifficulty(gameId))
 
-  const categorySet = new Set()
-  for (let item of items) {
-    categorySet.add(item.category)
-  }
-  const categories = Array.from(categorySet).sort()
+  const inventory: string[] = selectInventory(gameId)(store.getState())
+
+  const [categories, setCategories] = useState>([])
+  const [modifiedItems, setModifiedItems] = useState>([])
+  const [recentItems, setRecentItems] = useState>([])
+
+
+  useEffect(() => {
+    const categorySet = new Set()
+
+    if (!items) {return}
+    for (let item of items) {
+      categorySet.add(item.category)
+    }
+    setCategories(Array.from(categorySet).sort())
 
-  // Add inventory items from local store as unlocked.
-  // Items are unlocked if they are in the local store, or if the server says they should be
-  // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different
-  // modi)
-  let inv: string[] = selectInventory(gameId)(store.getState())
-  let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile)
+    // Add inventory items from local store as unlocked.
+    // Items are unlocked if they are in the local store, or if the server says they should be
+    // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different
+    // modi)
+    let _modifiedItems : InventoryTile[] = items?.map(tile => inventory.includes(tile.name) ? {...tile, locked: false} : tile)
+    setModifiedItems(_modifiedItems)
+    // Item(s) proved in the preceeding level
+    setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1))
 
-  // Item(s) proved in the preceeding level
-  let recentItems = modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1)
+  }, [items, inventory])
 
   return <>
-    {categories.length > 1 &&
+    { categories.length > 1 &&
       

         {categories.map((cat) => {
           let hasNew = modifiedItems.filter(item => item.new && (cat == item.category)).length > 0
@@ -97,91 +127,109 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
       {[...modifiedItems].sort(
           // For lemas, sort entries `available > disabled > locked`
           // otherwise alphabetically
-          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
+          (x, y) => +(categoryTab == "theorem") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
         ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
             return  {openDoc({name: item.name, type: docType})}}
+              showDoc={() => {setDocTile(item)}}
               name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
               disabled={item.disabled}
               recent={recentItems.map(x => x.name).includes(item.name)}
-              newly={item.new} enableAll={enableAll} />
+              newly={item.new} />
         })
       }
     

     
 }
 
-function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false, enableAll=false}) {
-  const icon = locked ?  :
-               disabled ?  : item.st
-  const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
-  // Note: This is somewhat a hack as the statement of lemmas comes currently in the form
-  // `Namespace.statement_name (x y : Nat) : some type`
-  const title = locked ? t("Not unlocked yet") :
-                disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
 
-  const [copied, setCopied] = useState(false)
 
-  const handleClick = () => {
-    if (enableAll || !locked) {
-      showDoc()
-    }
-  }
+/** The `Inventory` shows all items present in the game sorted by item type. */
+export function Inventory () {
+  const { t } = useTranslation()
 
-  const copyItemName = (ev) => {
-    navigator.clipboard.writeText(displayName)
-    setCopied(true)
-    setInterval(() => {
-      setCopied(false)
-    }, 3000);
-    ev.stopPropagation()
+  const { gameId, worldId, levelId } = React.useContext(GameIdContext)
+  const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+
+  let { theoremTab, setTheoremTab, categoryTab, setCategoryTab } = useContext(InventoryContext)
+
+  /** Helper function to find if a list of tiles comprises any new elements. */
+  function containsNew(tiles: InventoryTile[]) {
+    console.log(tiles)
+    return tiles?.filter(item => item.new).length > 0
   }
 
-return 

-    {icon} {displayName}
-    

-      {copied ?  : }
+  return (
+    

+      { levelInfo.data ? <>
+      

+        
 { setCategoryTab("theorem") }}>{t("Theorems")}

+        
 { setCategoryTab("tactic") }}>{t("Tactics")}

+        
 { setCategoryTab("definition") }}>{t("Definitions")}

+      

+      { (categoryTab == "theorem") &&
+        
+      }
+      { (categoryTab == "tactic") &&
+        
+      }
+      { (categoryTab == "definition") &&
+        
+      }
+     :  }
     

-  

+  )
 }
 
-export function Documentation({name, type, handleClose}) {
-  const {gameId} = React.useContext(GameIdContext)
-  const doc = useLoadDocQuery({game: gameId, type: type, name: name})
+/** The `documentation` */
+export function Documentation() {
+  const { gameId } = React.useContext(GameIdContext)
+  // const docEntry = useLoadDocQuery({game: gameId, type: type, name: name})
+  let { docTile, setDocTile } = useContext(InventoryContext)
+
+  const docEntry = useLoadDocQuery({game: gameId, name: docTile.name})
+
+
+  // Set `inventoryDoc` to `null` to close the doc
+  function closeInventoryDoc() { setDocTile(null) }
 
   return 

-    

-    
{doc.data?.displayName}

-    
{doc.data?.statement}

-    {/* docstring: {doc.data?.docstring} */}
-    {t(doc.data?.content, {ns: gameId})}
+    
+    
{docTile.data?.displayName}

+    
{docEntry.data?.statement}

+    {t(docEntry.data?.content, {ns: gameId})}
   

 }
 
-/** 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 [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab)
+/** The panel showing the user's inventory with tactics, definitions, and lemmas */
+export function InventoryPanel({visible = true}) {
+  const {gameId, worldId, levelId} = React.useContext(GameIdContext)
+  const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+  const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
+  const [theoremTab, setTheoremTab] = useState(null)
+  const [categoryTab, setCategoryTab] = useState<"tactic"|"theorem"|"definition">('tactic')
   // The inventory is overlayed by the doc entry of a clicked item
-  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
-  // Set `inventoryDoc` to `null` to close the doc
-  function closeInventoryDoc() {setInventoryDoc(null)}
+  const [docTile, setDocTile] = useState(null)
 
-    useEffect(() => {
+  useEffect(() => {
     // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
     // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
-    if (levelInfo?.lemmaTab) {
-      setLemmaTab(levelInfo?.lemmaTab)
+    if (levelInfo?.data?.lemmaTab) {
+      setTheoremTab(levelInfo?.data?.lemmaTab)
     }}, [levelInfo])
 
   return 

-    {inventoryDoc ?
-      
+    
+    {docTile ?
+      
       :
-      
+      
     }
+    
   

 }
+
+// HERE: next up: locked items should not be disabled!
diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx
index c14e3df..42a3649 100644
--- a/client/src/components/landing_page.tsx
+++ b/client/src/components/landing_page.tsx
@@ -109,23 +109,26 @@ function LandingPage() {
         

       

     
-    

-      {allTiles.filter(x => x != null).length == 0 ?
-        

-          
-            No Games loaded. Use http://localhost:3000/#/g/local/FOLDER to open a
-            game directly from a local folder.
-          
-        

-        : lean4gameConfig.allGames.map((id, i) => (
-          
-        ))
-      }
-    

+    
+      

+
+        {allTiles.filter(x => x != null).length == 0 ?
+          

+            
+              No Games loaded. Use http://localhost:3000/#/g/local/FOLDER to open a
+              game directly from a local folder.
+            
+          

+          : lean4gameConfig.allGames.map((id, i) => (
+            
+          ))
+        }
+      

+    
     

       

         
{t("Development notes")}

diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 8dbd0a2..0a61790 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -53,12 +53,13 @@ import { InfoPopup } from './popup/info'
 import { PreferencesPopup } from './popup/preferences'
 import { useTranslation } from 'react-i18next'
 import i18next from 'i18next'
+import { ChatButtons } from './chat'
 
 
 monacoSetup()
 
-function Level() {
-  const params = useParams()
+export function Level({visible = true}) {
+  // const params = useParams()
   // const levelId = parseInt(params.levelId)
   // const worldId = params.worldId
 
@@ -87,11 +88,11 @@ function Level() {
 
   useEffect(() => {}, [])
 
-  return 
-    {levelId == 0 ?
-       :
-      }
-  
+  return 

+    
+      
+    
+  

 }
 
 function ChatPanel({lastLevel, visible = true}) {
@@ -199,7 +200,7 @@ function ChatPanel({lastLevel, visible = true}) {
 }
 
 
-function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject, visible?: boolean}) {
+export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject, visible?: boolean}) {
   const {gameId} = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -211,7 +212,7 @@ function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableR
   

 }
 
-function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo, togglePreferencesPopup}) {
+export function PlayableLevel() {
   let { t } = useTranslation()
   const codeviewRef = useRef(null)
   const {gameId} = React.useContext(GameIdContext)
@@ -248,9 +249,9 @@ function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo
   const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
 
-  // impressum pop-up
-  function toggleImpressum() {setImpressum(!impressum)}
-  function togglePrivacy() {setPrivacy(!privacy)}
+  // // impressum pop-up
+  // function toggleImpressum() {setImpressum(!impressum)}
+  // function togglePrivacy() {setPrivacy(!privacy)}
 
   // When clicking on an inventory item, the inventory is overlayed by the item's doc.
   // If this state is set to a pair `(name, type)` then the according doc will be open.
@@ -424,24 +425,7 @@ function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo
                     toggleInfo={toggleInfo}
                   togglePreferencesPopup={togglePreferencesPopup}
                   /> */}
-                {mobile?
-                  // TODO: This is copied from the `Split` component below...
-                  <>
-                    

-                      
-                      
-                    

-                  
-                :
-                  
-                    
-                    
-                    
-                  
-                }
+                
               
             
           
@@ -451,6 +435,11 @@ function PlayableLevel({impressum, setImpressum, privacy, setPrivacy, toggleInfo
   
 }
 
+  // 
+  // 
+  // 
+  // 
+
 function IntroductionPanel({gameInfo}) {
   let { t } = useTranslation()
   const {gameId} = React.useContext(GameIdContext)
@@ -466,21 +455,14 @@ function IntroductionPanel({gameInfo}) {
           hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
       ))}
     

-    

-      {gameInfo.data?.worldSize[worldId] == 0 ?
-         :
-        
-      }
-    

+
} export default Level /** The site with the introduction text of a world */ -function Introduction({impressum, setImpressum, privacy, setPrivacy, toggleInfo, togglePreferencesPopup}) { +function Introduction() { let { t } = useTranslation() const {gameId} = React.useContext(GameIdContext) @@ -495,12 +477,12 @@ function Introduction({impressum, setImpressum, privacy, setPrivacy, toggleInfo, let image: string = gameInfo.data?.worlds.nodes[worldId].image - const toggleImpressum = () => { - setImpressum(!impressum) - } - const togglePrivacy = () => { - setPrivacy(!privacy) - } + // const toggleImpressum = () => { + // setImpressum(!impressum) + // } + // const togglePrivacy = () => { + // setPrivacy(!privacy) + // } return <> {/* */} {gameInfo.isLoading ? @@ -508,16 +490,16 @@ function Introduction({impressum, setImpressum, privacy, setPrivacy, toggleInfo, : mobile ? : - - + // + //
{image && }
- - + // {/* */} + // } diff --git a/client/src/components/navigation.tsx b/client/src/components/navigation.tsx index 7eb48c3..522b74b 100644 --- a/client/src/components/navigation.tsx +++ b/client/src/components/navigation.tsx @@ -12,9 +12,10 @@ import { useTranslation } from 'react-i18next' import '../css/navigation.css' import { PopupContext } from './popup/popup' import { useSelector } from 'react-redux' -import { selectProgress } from '../state/progress' +import { selectCompleted, selectDifficulty, selectProgress } from '../state/progress' import lean4gameConfig from '../config.json' import { Flag } from './flag' +import { useAppSelector } from '../hooks' /** SVG github icon */ function GithubIcon () { @@ -119,6 +120,8 @@ function DesktopNavigationLevel () { const { typewriterMode, setTypewriterMode, lockEditorMode } = useContext(PageContext) const gameInfo = useGetGameInfoQuery({game: gameId}) const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const difficulty = useSelector(selectDifficulty(gameId)) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) /** toggle input mode if allowed */ function toggleInputMode(ev: React.MouseEvent) { @@ -151,32 +154,34 @@ function DesktopNavigationLevel () {
- { levelId > 0 && - - } - { levelId == gameInfo.data?.worldSize[worldId] ? - : - - } - { levelId > 0 && - toggleInputMode(ev)} - title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} /> - } + { levelId > 0 && + + } + { levelId == gameInfo.data?.worldSize[worldId] ? + : + + } + { levelId > 0 && + toggleInputMode(ev)} + title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} /> + }
} @@ -203,9 +208,9 @@ function MobileNavigationLevel () {
setPage(page?0:1)} - inverted={true}/> + icon={(page == 1) ? faBook : faBookOpen} + onClick={() => setPage((page == 1) ? 2 : 1)} + inverted={true} />
} @@ -213,17 +218,29 @@ function MobileNavigationLevel () { /** The skeleton of the navigation which is the same across all layouts. */ export function Navigation () { const { t, i18n } = useTranslation() - const { gameId, worldId } = useContext(GameIdContext) + const { gameId, worldId, levelId } = useContext(GameIdContext) const { mobile, language, setLanguage } = useContext(PreferencesContext) const { setPopupContent } = useContext(PopupContext) + const { typewriterMode, setTypewriterMode, lockEditorMode } = useContext(PageContext) const gameProgress = useSelector(selectProgress(gameId)) const gameInfo = useGetGameInfoQuery({game: gameId}) + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const difficulty = useSelector(selectDifficulty(gameId)) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) const [navOpen, setNavOpen] = useState(false) const [langNavOpen, setLangNavOpen] = useState(false) function toggleNav () {setNavOpen(!navOpen); setLangNavOpen(false)} function toggleLangNav () {setLangNavOpen(!langNavOpen); setNavOpen(false)} + /** toggle input mode if allowed */ + function toggleInputMode(ev: React.MouseEvent) { + if (!lockEditorMode) { + setTypewriterMode(!typewriterMode) + console.log('test') + } + } + return