import * as React from 'react'; import { useState, useEffect } from 'react'; import './inventory.css' 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, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api'; import { selectDifficulty, selectInventory } from '../state/progress'; import { store } from '../state/store'; import { useSelector } from 'react-redux'; export function Inventory({levelInfo, openDoc, enableAll=false} : { levelInfo: LevelInfo|InventoryOverview, openDoc: (props: {name: string, type: string}) => void, enableAll?: boolean, }) { return (
{/* TODO: Click on Tactic: show info TODO: click on paste icon -> paste into command line */}

Tactics

{levelInfo?.tactics && }

Definitions

{levelInfo?.definitions && }

Theorems

{levelInfo?.lemmas && }
) } function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} : { items: InventoryTile[], docType: string, openDoc(props: {name: string, type: string}): void, defaultTab? : string, level? : LevelInfo|InventoryOverview, enableAll?: boolean, }) { // 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 difficulty = useSelector(selectDifficulty(gameId)) const categorySet = new Set() for (let item of items) { categorySet.add(item.category) } const categories = Array.from(categorySet).sort() const [tab, setTab] = useState(defaultTab) // 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) 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 (defaultTab) { setTab(defaultTab) }}, [level]) return <> {categories.length > 1 &&
{categories.map((cat) =>
{ setTab(cat) }}>{cat}
)}
}
{[...modifiedItems].sort( // For lemas, sort entries `available > disabled > locked` // otherwise alphabetically (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => { return {openDoc({name: item.name, type: docType})}} name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false} disabled={item.disabled} newly={item.new} enableAll={enableAll}/> }) }
} function InventoryItem({name, displayName, locked, disabled, newly, showDoc, enableAll=false}) { const icon = locked ? : disabled ? : "" const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : "" const title = locked ? "Not unlocked yet" : disabled ? "Not available in this level" : "" const handleClick = () => { if (enableAll || !locked) { showDoc() } } return
{icon} {displayName}
} export function Documentation({name, type, handleClose}) { const gameId = React.useContext(GameIdContext) const doc = useLoadDocQuery({game: gameId, type: type, name: name}) return

{doc.data?.displayName}

{doc.data?.statement}

{/* docstring: {doc.data?.docstring} */} {doc.data?.content}
} /** 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) // 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 ? : }
}