diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
index b26ecf1..0adf55d 100644
--- a/client/src/components/inventory.tsx
+++ b/client/src/components/inventory.tsx
@@ -12,6 +12,7 @@ import { store } from '../state/store';
import { useSelector } from 'react-redux';
import { useTranslation } from 'react-i18next';
import { t } from 'i18next';
+import { WorldLevelIdContext } from './infoview/context';
export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
{
@@ -57,6 +58,7 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
// been loaded. Is there a better way to observe this?
const gameId = React.useContext(GameIdContext)
+ const {worldId, levelId} = React.useContext(WorldLevelIdContext)
const difficulty = useSelector(selectDifficulty(gameId))
@@ -73,12 +75,15 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
let inv: string[] = selectInventory(gameId)(store.getState())
let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile)
+ // Item(s) proved in the preceeding level
+ let recentItems = modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1)
+
return <>
{categories.length > 1 &&
{categories.map((cat) => {
let hasNew = modifiedItems.filter(item => item.new && (cat == item.category)).length > 0
- return
x.category).includes(cat) ? ' recent': ''}`}
onClick={() => { setTab(cat) }}>{cat}
})}
}
@@ -91,14 +96,16 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
item={item}
showDoc={() => {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} />
+ disabled={item.disabled}
+ recent={recentItems.map(x => x.name).includes(item.name)}
+ newly={item.new} enableAll={enableAll} />
})
}
>
}
-function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
+function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false, enableAll=false}) {
const icon = locked ? :
disabled ? : item.st
const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
@@ -124,7 +131,7 @@ function InventoryItem({item, name, displayName, locked, disabled, newly, showDo
ev.stopPropagation()
}
-return
+return
{icon} {displayName}
{copied ? : }
diff --git a/client/src/css/inventory.css b/client/src/css/inventory.css
index d3fc5b6..f18292c 100644
--- a/client/src/css/inventory.css
+++ b/client/src/css/inventory.css
@@ -46,6 +46,9 @@
background-color: rgb(255, 242, 190);
}
+.inventory .item.recent {
+ background-color: rgb(242, 190, 255);
+}
.inventory .item:not(.locked), .inventory .item.enabled {
cursor: pointer;
}
@@ -72,6 +75,14 @@
border-bottom: 0.3em solid var(--clr-primary);
}
+.inventory .tab.recent {
+ background-image: linear-gradient(to bottom, rgba(255,0,0,0), rgb(242, 190, 255));
+}
+
+.inventory .tab.recent:not(.active) {
+ border-bottom: 0.3em solid rgb(242, 190, 255);
+}
+
.inventory .tab.new {
background-image: linear-gradient(to bottom, rgba(255,0,0,0), rgb(255, 242, 190));
}
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index 1a64597..8a88119 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -36,6 +36,9 @@ export interface InventoryTile {
new: boolean,
hidden: boolean
altTitle: string,
+ world : string|null,
+ level : number|null,
+ proven : boolean
}
export interface LevelInfo {
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 76544f9..c2ba0a0 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -973,6 +973,10 @@ elab "MakeGame" : command => do
name := name
displayName := data.displayName
category := data.category
+ world := worldId
+ -- from the previous level. This is fine b/c in practise levels start at 1
+ level := (levelId - 1 : Nat)
+ proven := true
altTitle := data.statement
locked := false }
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index d2a47d5..d2b86c4 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -93,6 +93,12 @@ structure InventoryTile where
displayName : String
/-- Category to group inventory items by (currently only used for lemmas). -/
category : String
+ /-- The world which introduced this item. -/
+ world : Option Name := none
+ /-- The level which introduced this item. -/
+ level : Option Nat := none
+ /-- Set to `true` if there exists an exercise in the game proving this statement. -/
+ proven := false
/-- If `true` then the item only gets unlocked in a later level. -/
locked := true
/-- If `true` then the item is blocked for this level. -/