|
|
|
|
@ -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<React.SetStateAction<string>>,
|
|
|
|
|
categoryTab: "tactic"|"theorem"|"definition",
|
|
|
|
|
setCategoryTab: React.Dispatch<React.SetStateAction<"tactic"|"theorem"|"definition">>,
|
|
|
|
|
docTile: any,
|
|
|
|
|
setDocTile: React.Dispatch<React.SetStateAction<any>>
|
|
|
|
|
}>({
|
|
|
|
|
theoremTab: null,
|
|
|
|
|
setTheoremTab: () => {},
|
|
|
|
|
categoryTab: "tactic",
|
|
|
|
|
setCategoryTab: () => {},
|
|
|
|
|
docTile: null,
|
|
|
|
|
setDocTile: () => {}
|
|
|
|
|
})
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
*/
|
|
|
|
|
function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false }) {
|
|
|
|
|
const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
|
|
|
|
|
disabled ? <FontAwesomeIcon icon={faBan} /> : 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 (
|
|
|
|
|
<div className="inventory">
|
|
|
|
|
<div className="tab-bar major">
|
|
|
|
|
<div className={`tab${(tab == "theorem") ? " active": ""}${newTheorems ? " new" : ""}`} onClick={() => { setTab("theorem") }}>{t("Theorems")}</div>
|
|
|
|
|
<div className={`tab${(tab == "tactic") ? " active": ""}${newTactics ? " new" : ""}`} onClick={() => { setTab("tactic") }}>{t("Tactics")}</div>
|
|
|
|
|
<div className={`tab${(tab == "definition") ? " active": ""}${newDefinitions ? " new" : ""}`} onClick={() => { setTab("definition") }}>{t("Definitions")}</div>
|
|
|
|
|
</div>
|
|
|
|
|
{ (tab == "theorem") && levelInfo?.lemmas &&
|
|
|
|
|
<InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
|
|
|
|
|
}
|
|
|
|
|
{ (tab == "tactic") && levelInfo?.tactics &&
|
|
|
|
|
<InventoryList items={levelInfo?.tactics} docType="Tactic" openDoc={openDoc} enableAll={enableAll}/>
|
|
|
|
|
}
|
|
|
|
|
{ (tab == "definition") && levelInfo?.definitions &&
|
|
|
|
|
<InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} enableAll={enableAll}/>
|
|
|
|
|
}
|
|
|
|
|
const copyItemName = (ev) => {
|
|
|
|
|
navigator.clipboard.writeText(displayName)
|
|
|
|
|
setCopied(true)
|
|
|
|
|
setInterval(() => {
|
|
|
|
|
setCopied(false)
|
|
|
|
|
}, 3000);
|
|
|
|
|
ev.stopPropagation()
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
return <div className={`item ${className}${(difficulty == 0) ? ' enabled' : ''}${recent ? ' recent' : ''}`} onClick={handleClick} title={title}>
|
|
|
|
|
{icon} {displayName}
|
|
|
|
|
<div className="copy-button" onClick={copyItemName}>
|
|
|
|
|
{copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
|
|
|
|
|
</div>
|
|
|
|
|
)
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
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<React.SetStateAction<string>>
|
|
|
|
|
}) {
|
|
|
|
|
// 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<string>()
|
|
|
|
|
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<Array<string>>([])
|
|
|
|
|
const [modifiedItems, setModifiedItems] = useState<Array<InventoryTile>>([])
|
|
|
|
|
const [recentItems, setRecentItems] = useState<Array<InventoryTile>>([])
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
useEffect(() => {
|
|
|
|
|
const categorySet = new Set<string>()
|
|
|
|
|
|
|
|
|
|
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 &&
|
|
|
|
|
<div className="tab-bar">
|
|
|
|
|
{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 <InventoryItem key={`${item.category}-${item.name}`}
|
|
|
|
|
item={item}
|
|
|
|
|
showDoc={() => {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} />
|
|
|
|
|
})
|
|
|
|
|
}
|
|
|
|
|
</div>
|
|
|
|
|
</>
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false, enableAll=false}) {
|
|
|
|
|
const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
|
|
|
|
|
disabled ? <FontAwesomeIcon icon={faBan} /> : 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 <div className={`item ${className}${enableAll ? ' enabled' : ''}${recent ? ' recent' : ''}`} onClick={handleClick} title={title}>
|
|
|
|
|
{icon} {displayName}
|
|
|
|
|
<div className="copy-button" onClick={copyItemName}>
|
|
|
|
|
{copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
|
|
|
|
|
return (
|
|
|
|
|
<div className="inventory">
|
|
|
|
|
{ levelInfo.data ? <>
|
|
|
|
|
<div className="tab-bar major">
|
|
|
|
|
<div className={`tab${(categoryTab == "theorem") ? " active": ""}${containsNew(levelInfo.data?.lemmas) ? " new" : ""}`} onClick={() => { setCategoryTab("theorem") }}>{t("Theorems")}</div>
|
|
|
|
|
<div className={`tab${(categoryTab == "tactic") ? " active": ""}${containsNew(levelInfo.data?.tactics) ? " new" : ""}`} onClick={() => { setCategoryTab("tactic") }}>{t("Tactics")}</div>
|
|
|
|
|
<div className={`tab${(categoryTab == "definition") ? " active": ""}${containsNew(levelInfo.data?.definitions) ? " new" : ""}`} onClick={() => { setCategoryTab("definition") }}>{t("Definitions")}</div>
|
|
|
|
|
</div>
|
|
|
|
|
{ (categoryTab == "theorem") &&
|
|
|
|
|
<InventoryList items={levelInfo.data?.lemmas} tab={theoremTab} setTab={setTheoremTab} />
|
|
|
|
|
}
|
|
|
|
|
{ (categoryTab == "tactic") &&
|
|
|
|
|
<InventoryList items={levelInfo.data?.tactics} />
|
|
|
|
|
}
|
|
|
|
|
{ (categoryTab == "definition") &&
|
|
|
|
|
<InventoryList items={levelInfo.data?.definitions} />
|
|
|
|
|
}
|
|
|
|
|
</> : <LoadingIcon /> }
|
|
|
|
|
</div>
|
|
|
|
|
</div>
|
|
|
|
|
)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
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 <div className="documentation">
|
|
|
|
|
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
|
|
|
|
<h1 className="doc">{doc.data?.displayName}</h1>
|
|
|
|
|
<p><code>{doc.data?.statement}</code></p>
|
|
|
|
|
{/* <code>docstring: {doc.data?.docstring}</code> */}
|
|
|
|
|
<Markdown>{t(doc.data?.content, {ns: gameId})}</Markdown>
|
|
|
|
|
<NavButton icon={faXmark}
|
|
|
|
|
onClick={closeInventoryDoc}
|
|
|
|
|
inverted={true} />
|
|
|
|
|
<h1 className="doc">{docTile.data?.displayName}</h1>
|
|
|
|
|
<p><code>{docEntry.data?.statement}</code></p>
|
|
|
|
|
<Markdown>{t(docEntry.data?.content, {ns: gameId})}</Markdown>
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/** 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<string>(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<InventoryTile>(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 <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
|
|
|
|
|
{inventoryDoc ?
|
|
|
|
|
<Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
|
|
|
|
|
<InventoryContext.Provider value={{theoremTab, setTheoremTab, categoryTab, setCategoryTab, docTile, setDocTile }}>
|
|
|
|
|
{docTile ?
|
|
|
|
|
<Documentation />
|
|
|
|
|
:
|
|
|
|
|
<Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true} lemmaTab={lemmaTab} setLemmaTab={setLemmaTab}/>
|
|
|
|
|
<Inventory />
|
|
|
|
|
}
|
|
|
|
|
</InventoryContext.Provider>
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// HERE: next up: locked items should not be disabled!
|
|
|
|
|
|
Jon Eugster
9 months ago