add inventory to start page

client/src/components/inventory.tsx

@@ -5,11 +5,11 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
-import { useLoadDocQuery, InventoryTile, LevelInfo } from '../state/api';
+import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview } from '../state/api';
 
 export function Inventory({levelInfo, openDoc } :
   {
-    levelInfo: LevelInfo,
+    levelInfo: LevelInfo|InventoryOverview,
     openDoc: (name: string, type: string) => void,
   }) {
 
@@ -18,14 +18,17 @@ export function Inventory({levelInfo, openDoc } :
     {/* TODO: Click on Tactic: show info
       TODO: click on paste icon -> paste into command line */}
       <h2>Tactics</h2>
-      <InventoryList items={levelInfo?.tactics} docType="Tactic" openDoc={openDoc} />
+      {levelInfo?.tactics &&
-
+        <InventoryList items={levelInfo?.tactics} docType="Tactic" openDoc={openDoc} />
+      }
       <h2>Definitions</h2>
-      <InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} />
+      {levelInfo?.definitions &&
-
+        <InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} />
+      }
       <h2>Lemmas</h2>
-      <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc}
+      {levelInfo?.lemmas &&
-        defaultTab={levelInfo?.lemmaTab} level={levelInfo}/>
+        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo}/>
+      }
     </div>
   )
 }
@@ -36,7 +39,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
     docType: string,
     openDoc(name: string, type: string): void,
     defaultTab? : string,
-    level? : LevelInfo,
+    level? : LevelInfo|InventoryOverview,
   }) {
   // 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?

client/src/components/level.tsx

@@ -26,7 +26,7 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event';
 import type { Location } from 'vscode-languageserver-protocol';
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faHome, faCircleInfo, faArrowRight, faArrowLeft, faShield, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
+import { faBars, faHome, faCircleInfo, faArrowRight, faArrowLeft, faShield, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
 import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
 
 import { GameIdContext } from '../app';
@@ -235,7 +235,8 @@ function PlayableLevel({worldId, levelId}) {
   // Set `inventoryDoc` to `null` to close the doc
   const closeInventoryDoc = () => setInventoryDoc(null);
 
-  const levelTitle = <>{levelId && `Level ${levelId}`}{level?.data?.title && `: ${level?.data?.title}`}</>
+  const levelTitle = <>
+    {levelId && `Level ${levelId} / ${gameInfo.data?.worldSize[worldId]}`}{level?.data?.title && `: ${level?.data?.title}`}</>
 
   // TODO: with the new design, there is no difference between the introduction and
   // a hint at the beginning of the proof...
@@ -261,7 +262,7 @@ function PlayableLevel({worldId, levelId}) {
     <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
     <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
     <ProofContext.Provider value={{proof, setProof}}>
-      <LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} toggleImpressum={toggleImpressum}/>
+      <LevelAppBar isLoading={level.isLoading} levelTitle={`Level ${levelId} / ${gameInfo.data?.worldSize[worldId]}` + (level?.data?.title && ` : ${level?.data?.title}`)} worldId={worldId} levelId={levelId} toggleImpressum={toggleImpressum}/>
       <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
         <div className="chat-panel">
           <div ref={chatRef} className="chat">
@@ -292,7 +293,7 @@ function PlayableLevel({worldId, levelId}) {
                   </div>
                 }
                 {levelId >= gameInfo.data?.worldSize[worldId] ?
-                <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
+                <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /> Leave World</Button> :
                 <Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
                   Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>}
               </>
@@ -392,26 +393,40 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle, toggleImpressum})
 
   return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
     <div>
-      <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button>
+      <span className="app-bar-title">
-        <span className="app-bar-title">
+        {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
-          {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
+      </span>
-        </span>
+    </div>
-      </div>
     <div>
       <span className="app-bar-title">
         {levelTitle}
       </span>
-        <Button disabled={levelId <= 0} inverted="true" to="" onClick={(ev) => { setCommandLineMode(!commandLineMode) }}>
+        {levelId > 0 && <>
-          Editor
+          <Button disabled={levelId <= 0} inverted="true" to=""
-        </Button>
+              onClick={(ev) => { setCommandLineMode(!commandLineMode) }}
-        <Button disabled={levelId <= 0} inverted="true" to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}>
+              title="toggle Editor mode">
-          <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
+            Editor
+          </Button>
+          <Button disabled={levelId <= 0} inverted="true"
+              to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
+              title="previous level">
+            <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
+          </Button>
+        </>}
+        {levelId < gameInfo.data?.worldSize[worldId] &&
+          <Button inverted="true" to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level">
+            Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+          </Button>
+        }
+
+        <Button title="information, Impressum, privacy policy" inverted="true" to="" onClick={toggleImpressum}>
+          <FontAwesomeIcon icon={faCircleInfo} /> Info &amp; Impressum
         </Button>
-        <Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted="true" to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
+        <Button to={`/${gameId}`} inverted="true" title="back to world selection">
-          Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+          <FontAwesomeIcon icon={faHome} /> Home
         </Button>
-        <Button title="Information, Impressum, Privacy Policy" inverted="true" to="" onClick={toggleImpressum}>
+        <Button to="" inverted="true">
-          <FontAwesomeIcon icon={faCircleInfo} />
+          <FontAwesomeIcon icon={faBars} />
         </Button>
     </div>
 

client/src/components/welcome.tsx

@@ -12,11 +12,12 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faGlobe, faHome, faCircleInfo, faArrowRight, faArrowLeft, faShield, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';
 import { selectCompleted } from '../state/progress';
-import { useGetGameInfoQuery } from '../state/api';
+import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api';
 import Markdown from './markdown';
 import WorldSelectionMenu from './world_selection_menu';
 import {PrivacyPolicy} from './privacy_policy';
 import { Button } from './button';
+import { Documentation, Inventory } from './inventory';
 
 cytoscape.use( klay );
 
@@ -47,6 +48,20 @@ function Welcome() {
   const gameId = React.useContext(GameIdContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
+  const inventory = useLoadInventoryOverviewQuery({game: gameId})
+
+  // 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.
+  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
+
+  // Open the doc of the clicked inventory item
+  function openInventoryDoc(name, type) {
+    setInventoryDoc({name, type})
+  }
+
+  // Set `inventoryDoc` to `null` to close the doc
+  const closeInventoryDoc = () => setInventoryDoc(null);
+
   const { nodes, bounds }: any = gameInfo.data ? computeWorldLayout(gameInfo.data?.worlds) : {nodes: []}
 
   useEffect(() => {
@@ -100,7 +115,7 @@ function Welcome() {
       <CircularProgress />
     </Box>
     :
-    <Split className="welcome" minSize={200} sizes={[70, 30]}>
+    <Split className="welcome" minSize={200} sizes={[40, 35, 25]}>
       <div className="column">
         <Typography variant="body1" component="div" className="welcome-text">
           <Button inverted="false" title="back to games selection" to="/">
@@ -118,6 +133,15 @@ function Welcome() {
           </svg>
         </Box>
       </div>
+      <div className="inventory-panel">
+        {<>
+          {inventoryDoc ?
+            <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
+            :
+            <Inventory levelInfo={inventory.data} openDoc={openInventoryDoc} />
+          }
+        </>}
+      </div>
     </Split>
   }
     <PrivacyPolicy />

client/src/state/api.ts

@@ -36,6 +36,14 @@ export interface LevelInfo {
   statementName: null|string
 }
 
+/** Used to display the inventory on the welcome page */
+export interface InventoryOverview {
+  tactics: InventoryTile[],
+  lemmas: InventoryTile[],
+  definitions: InventoryTile[],
+  lemmaTab: null,
+}
+
 interface Doc {
   name: string,
   displayName: string,
@@ -74,6 +82,9 @@ export const apiSlice = createApi({
     loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
       query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}},
     }),
+    loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
+      query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}},
+    }),
     loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({
       query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}},
     }),
@@ -82,4 +93,4 @@ export const apiSlice = createApi({
 
 // Export hooks for usage in functional components, which are
 // auto-generated based on the defined endpoints
-export const { useGetGameInfoQuery, useLoadLevelQuery, useLoadDocQuery } = apiSlice
+export const { useGetGameInfoQuery, useLoadLevelQuery, useLoadDocQuery, useLoadInventoryOverviewQuery } = apiSlice

server/GameServer/Game.lean

@@ -51,6 +51,13 @@ structure LevelInfo where
   statementName : Option String
 deriving ToJson, FromJson
 
+structure InventoryOverview where
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  lemmaTab : Option String
+deriving ToJson, FromJson
+
 structure LoadLevelParams where
   world : Name
   level : Nat
@@ -141,7 +148,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       return true
     | Message.request id "loadDoc" params =>
       let p ← parseParams LoadDocParams (toJson params)
-      -- let s ← get
+      let s ← get
       let c ← read
       let some doc ← getInventoryItem? p.name p.type
         | do
@@ -154,6 +161,29 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       --   name := doc.name.toString }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
       return true
+    | Message.request id "loadInventoryOverview" _ =>
+      let s ← get
+      let some game ← getGame? s.game
+        | return false
+      -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world
+      -- and reset `new`, `disabled` and `unlocked`
+      match game.worlds.nodes.toList with
+      | [] => return false
+      | ⟨worldId, _⟩ :: _ =>
+        let some lvl ← getLevel? {game := s.game, world := worldId, level := 1}
+          | do return false
+        let inventory : InventoryOverview := {
+          tactics := lvl.tactics.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          lemmas := lvl.lemmas.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          definitions := lvl.definitions.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          lemmaTab := none
+        }
+        let c ← read
+        c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩
+        return true
     | _ => return false
   | _ => return false