diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index a358e5bc..b2432a08 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -5,7 +5,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faBan } from '@fortawesome/free-solid-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, WorldOverview } from '../state/api'; import { selectDifficulty, selectInventory } from '../state/progress'; import { store } from '../state/store'; import { useSelector } from 'react-redux'; @@ -37,6 +37,79 @@ export function Inventory({levelInfo, openDoc, enableAll=false} : ) } +export function OverviewInventory({data, openDoc, enableAll=false, showOverview=true} : + { + data: WorldOverview[], + openDoc: (props: {name: string, type: string}) => void, + enableAll?: boolean, + showOverview?: boolean + }) { + + const gameId = React.useContext(GameIdContext) + const difficulty = useSelector(selectDifficulty(gameId)) + const [tab, setTab] = useState() + let inv: string[] = selectInventory(gameId)(store.getState()) + + let levelInfo : InventoryOverview = { + tactics : data ? data.map(world => (world.tactics.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [], + lemmas : data ? data.map(world => (world.lemmas.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [], + definitions : data ? data.map(world => (world.definitions.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [], + lemmaTab: null, + } + + return ( + <> + + {showOverview && +
+ {data && <> +

Overviews

+
+ {data.map(world => { + return
{ setTab((tab == world.world) ? null : world.world) }}>{world.world}
+ })} +
+
+ {/* TODO: a bit hacky, do we need to redesign inventory completely and provide it in a better order? */} + {data.map(world => { + if (world.world == tab) { + return [ + ...world.tactics.map(item => { + return {openDoc({name: item.name, type: 'Tactic'})}} + name={item.name} displayName={item.displayName} + locked={difficulty > 0 ? !inv.includes(item.name) : false} + disabled={item.disabled} newly={false} enableAll={enableAll} /> + }), + ...world.lemmas.map(item => { + return {openDoc({name: item.name, type: 'Lemma'})}} + name={item.name} displayName={item.displayName} + locked={difficulty > 0 ? item.locked : false} + disabled={item.disabled} newly={false} enableAll={enableAll} /> + }), + ...world.definitions.map(item => { + return {openDoc({name: item.name, type: 'Definition'})}} + name={item.name} displayName={item.displayName} + locked={difficulty > 0 ? item.locked : false} + disabled={item.disabled} newly={false} enableAll={enableAll} /> + }) + ] + } + })} +
+ } +
+ } + + + ) +} + function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} : { items: InventoryTile[], @@ -144,3 +217,21 @@ export function InventoryPanel({levelInfo, visible = true}) { } } + +/** The panel (on the welcome page) showing the user's inventory with tactics, definitions, and lemmas */ +export function InventoryOverviewPanel({data, visible = true, showOverview=true} : {data : WorldOverview[], visible?: boolean, showOverview?: boolean}) { + const gameId = React.useContext(GameIdContext) + + // 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)} + + return
+ {inventoryDoc ? + + : + + } +
+} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 1251645b..579b9470 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -26,7 +26,7 @@ import { changedSelection, codeEdited, selectCode, selectSelections, selectCompl import { store } from '../state/store' import { Button } from './button' import Markdown from './markdown' -import {InventoryPanel} from './inventory' +import {InventoryOverviewPanel, InventoryPanel} from './inventory' import { hasInteractiveErrors } from './infoview/typewriter' import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context' @@ -498,7 +498,7 @@ function Introduction({impressum, setImpressum}) { } - + } diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index 6c6c9773..cc2e0af1 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -11,7 +11,7 @@ import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api' import { Button } from './button' import { MobileContext } from './infoview/context' -import { InventoryPanel } from './inventory' +import { InventoryOverviewPanel, InventoryPanel } from './inventory' import { ErasePopup } from './popup/erase' import { InfoPopup } from './popup/game_info' import { PrivacyPolicyPopup } from './popup/privacy_policy' @@ -111,7 +111,7 @@ function Welcome() { : - + )} : @@ -119,7 +119,7 @@ function Welcome() { - + } diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 2bdbe8b2..ed17d056 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -71,6 +71,13 @@ interface Doc { category: string, } +export interface WorldOverview { + world: string + tactics: InventoryTile[] + lemmas: InventoryTile[] + definitions: InventoryTile[] +} + // Define a service using a base URL and expected endpoints export const apiSlice = createApi({ reducerPath: 'gameApi', @@ -82,7 +89,7 @@ export const apiSlice = createApi({ loadLevel: builder.query({ query: ({game, world, level}) => `${game}/level__${world}__${level}.json`, }), - loadInventoryOverview: builder.query({ + loadInventoryOverview: builder.query({ query: ({game}) => `${game}/inventory.json`, }), loadDoc: builder.query({ diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index a1e15f32..bfb72e7c 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -269,6 +269,13 @@ structure GameLevel where image : String := default deriving Inhabited, Repr +structure WorldOverview where + world: Name + tactics: Array InventoryTile := default + definitions: Array InventoryTile := default + lemmas: Array InventoryTile := default + deriving FromJson, ToJson, Inhabited, Repr + /-- Json-encodable version of `GameLevel` Fields: - description: Lemma in mathematical language. diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean index fb59fdb1..06c546ef 100644 --- a/server/GameServer/Game.lean +++ b/server/GameServer/Game.lean @@ -93,6 +93,54 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do fw.stdin.writeLspMessage msg return true + | Message.request id "loadInventoryOverview" _ => + let s ← get + let some game ← getGame? s.game + | return false + + let mut overview : Array WorldOverview := #[] + for ⟨worldId, world⟩ in game.worlds.nodes.toList do + let mut tactics : Array InventoryTile := #[] + let mut theorems : Array InventoryTile := #[] + let mut definitions : Array InventoryTile := #[] + for ⟨_levelId, lvl⟩ in world.levels.toList do + tactics := tactics ++ lvl.tactics.tiles.filterMap (fun tile => match tile.new with + | true => some {tile with new := false, locked := true, disabled := false} + | false => none) + theorems := theorems ++ lvl.lemmas.tiles.filterMap (fun tile => match tile.new with + | true => some {tile with new := false, locked := true, disabled := false} + | false => none) + definitions := definitions ++ lvl.definitions.tiles.filterMap (fun tile => match tile.new with + | true => some {tile with new := false, locked := true, disabled := false} + | false => none) + overview := overview.push { + world := worldId, + tactics := tactics, + lemmas := theorems, + definitions := definitions } + let c ← read + c.hOut.writeLspResponse ⟨id, ToJson.toJson overview⟩ + return true + -- -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world + -- -- and reset `new`, `disabled` and `unlocked`. + -- -- Note: as we allow worlds without any levels (for developing), we might need + -- -- to try until we find the first world with levels. + -- for ⟨worldId, _⟩ in game.worlds.nodes.toList do + -- let some lvl ← getLevel? {game := s.game, world := worldId, level := 1} + -- | do continue + -- 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 | _ => return false