import * as React from 'react'; import { useState, useEffect } from 'react'; import '../css/inventory.css' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faBan, faCheck } 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 { selectDifficulty, selectInventory } from '../state/progress'; import { store } from '../state/store'; import { useSelector } from 'react-redux'; 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, }) { 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, tab=null, setTab=undefined, level=undefined, enableAll=false} : { items: InventoryTile[], docType: string, openDoc(props: {name: string, type: string}): void, tab?: any, setTab?: any, 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() // 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) 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) || x.displayName.localeCompare(y.displayName) ).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({item, name, displayName, locked, disabled, newly, showDoc, 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 ? "Not unlocked yet" : disabled ? "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() } } const copyItemName = (ev) => { navigator.clipboard.writeText(displayName) setCopied(true) setInterval(() => { setCopied(false) }, 3000); ev.stopPropagation() } return
{icon} {displayName}
{copied ? : }
} 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) const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab) // 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)} 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) }}, [levelInfo]) return
{inventoryDoc ? : }
}