From a783e1dffc61280c94b586c0f051e2fe9f88d214 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 2 Mar 2023 12:15:34 +0100 Subject: [PATCH] Add tabs for lemmas #23 --- client/src/app.css | 1 + client/src/components/Inventory.tsx | 61 ++++++++++++------- client/src/components/inventory.css | 22 +++++++ client/src/state/api.ts | 13 +++- server/leanserver/GameServer/Commands.lean | 27 +++++--- .../leanserver/GameServer/EnvExtensions.lean | 9 +-- server/leanserver/GameServer/Game.lean | 12 ++-- 7 files changed, 103 insertions(+), 42 deletions(-) diff --git a/client/src/app.css b/client/src/app.css index 3a13568..118b466 100644 --- a/client/src/app.css +++ b/client/src/app.css @@ -4,6 +4,7 @@ --clr-primary: #1976d2; --clr-light-gray: #ddd; --clr-dark-gray: #aaa; + --clr-darker-gray: #555; --clr-code: rgba(0, 32, 90, 0.87); --ff-primary: Roboto; --ff-code: "Roboto Mono"; diff --git a/client/src/components/Inventory.tsx b/client/src/components/Inventory.tsx index b3b6aaf..ab2b0f3 100644 --- a/client/src/components/Inventory.tsx +++ b/client/src/components/Inventory.tsx @@ -4,47 +4,66 @@ import './inventory.css' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons' import Markdown from './Markdown'; -import { useLoadDocQuery } from '../state/api'; +import { useLoadDocQuery, ComputedInventoryItem } from '../state/api'; function Inventory({ tactics, lemmas, definitions } : - {lemmas: {name: string, locked: boolean, disabled: boolean}[], - tactics: {name: string, locked: boolean, disabled: boolean}[], - definitions: {name: string, locked: boolean, disabled: boolean}[]}) { + {lemmas: ComputedInventoryItem[], + tactics: ComputedInventoryItem[], + definitions: ComputedInventoryItem[]}) { const [docName, setDocName] = useState(null) const [docType, setDocType] = useState(null) + function openDoc(name, type) { + setDocName(name) + setDocType(type) + } return (
+ {/* TODO: Click on Tactic: show info + TODO: click on paste icon -> paste into command line */}

Tactics

-
- { tactics.map(tac => - {setDocName(tac.name); setDocType("Tactic")}} - name={tac.name} locked={tac.locked} disabled={tac.disabled} />) } - {/* TODO: Click on Tactic: show info - TODO: click on paste icon -> paste into command line */} -
+

Definitions

-
- { definitions.map(def => - {setDocName(def.name); setDocType("Definition")}} - name={def.name} locked={def.locked} disabled={def.disabled} />) } -
+

Lemmas

-
- { lemmas.map(lem => - {setDocName(lem.name); setDocType("Lemma")}} - name={lem.name} locked={lem.locked} disabled={lem.disabled} />) } -
+ {docName && }
) } +function InventoryList({items, docType, openDoc} : {items: ComputedInventoryItem[], docType: string, openDoc(name: string, type: string): void}) { + + const categorySet = new Set() + for (let item of items) { + categorySet.add(item.category) + } + const categories = Array.from(categorySet).sort() + + const [tab, setTab] = useState(categories[0]); + + return <> + {categories.length > 1 && +
+ {categories.map((cat) => +
{ setTab(cat) }}>{cat}
)} +
} +
+ { items.map(item => { + if (tab == item.category) { + return {openDoc(item.name, docType)}} + name={item.name} locked={item.locked} disabled={item.disabled} /> + } + }) } +
+ +} + function InventoryItem({name, locked, disabled, showDoc}) { const icon = locked ? : disabled ? : "" diff --git a/client/src/components/inventory.css b/client/src/components/inventory.css index 3637093..4f89ca2 100644 --- a/client/src/components/inventory.css +++ b/client/src/components/inventory.css @@ -36,3 +36,25 @@ .inventory .item:not(.locked):not(.disabled) { cursor: pointer; } + +.tab-bar { + border-bottom: 0.1em solid var(--clr-dark-gray); + margin-bottom: 0.5em; +} + +.tab { + color: var(--clr-darker-gray); + line-height: inherit; + text-decoration: none; + padding: 0.2rem .6em; + font-size: 1rem; + margin: 0 .1em; + border: 0; + cursor: pointer; + display: inline-block; +} + +.tab.active { + color: black; + border-bottom: 0.3em solid var(--clr-primary); +} diff --git a/client/src/state/api.ts b/client/src/state/api.ts index c78b03e..713f4f8 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -10,13 +10,20 @@ interface GameInfo { conclusion: null|string, } +export interface ComputedInventoryItem { + name: string, + category: string, + disabled: boolean, + locked: boolean +} + interface LevelInfo { title: null|string, introduction: null|string, index: number, - tactics: {name: string, disabled: boolean, locked: boolean}[], - lemmas: {name: string, disabled: boolean, locked: boolean}[], - definitions: {name: string, disabled: boolean, locked: boolean}[], + tactics: ComputedInventoryItem[], + lemmas: ComputedInventoryItem[], + definitions: ComputedInventoryItem[], descrText: null|string, descrFormat: null|string, } diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 97c131e..8d08e6e 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -288,7 +288,7 @@ def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo | .Definition => level.definitions | .Lemma => level.lemmas -def GameLevel.setComputedInventory (level : GameLevel) : InventoryType → Array Availability → GameLevel +def GameLevel.setComputedInventory (level : GameLevel) : InventoryType → Array ComputedInventoryItem → GameLevel | .Tactic, v => {level with tactics := {level.tactics with computed := v}} | .Definition, v => {level with definitions := {level.definitions with computed := v}} | .Lemma, v => {level with lemmas := {level.lemmas with computed := v}} @@ -314,19 +314,28 @@ elab "MakeGame" : command => do newItemsInWorld := newItemsInWorld.insert worldId newItems -- Basic inventory item availability: all locked, none disabled. - let Availability₀ : HashMap Name Availability := + let Availability₀ : HashMap Name ComputedInventoryItem := HashMap.ofList $ - allItems.toList.map fun name => - (name, {name, locked := true, disabled := false}) + ← allItems.toList.mapM fun name => do + return (name, { + name + category := (← getInventoryDoc? name inventoryType).get!.category + locked := true + disabled := false}) -- Availability after a given world - let mut itemsInWorld : HashMap Name (HashMap Name Availability) := {} + let mut itemsInWorld : HashMap Name (HashMap Name ComputedInventoryItem) := {} for (worldId, _) in game.worlds.nodes.toArray do let mut items := Availability₀ let predecessors := game.worlds.predecessors worldId for predWorldId in predecessors do for item in newItemsInWorld.find! predWorldId do - items := items.insert item {name := item, locked := false, disabled := false} + items := items.insert item { + name := item + category := (← getInventoryDoc? item inventoryType).get!.category + locked := false + disabled := false + } itemsInWorld := itemsInWorld.insert worldId items for (worldId, world) in game.worlds.nodes.toArray do @@ -336,9 +345,11 @@ elab "MakeGame" : command => do for (levelId, level) in levels do for item in (level.getInventory inventoryType).new do - items := items.insert item {name := item, locked := false, disabled := false} + let category := (← getInventoryDoc? item inventoryType).get!.category + items := items.insert item {name := item, category, locked := false, disabled := false} for item in (level.getInventory inventoryType).disabled do - items := items.insert item {name := item, locked := false, disabled := true} + let category := (← getInventoryDoc? item inventoryType).get!.category + items := items.insert item {name := item, category, locked := false, disabled := true} let itemsArray := items.toArray |>.insertionSort (fun a b => a.1.toString < b.1.toString) diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 1469780..16fed62 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -30,7 +30,7 @@ structure GoalHintEntry where /-! ## Tactic/Definition/Lemma documentation -/ inductive InventoryType := | Tactic | Lemma | Definition -deriving ToJson, FromJson, Repr, BEq, Hashable +deriving ToJson, FromJson, Repr, BEq, Hashable, Inhabited instance : ToString InventoryType := ⟨fun t => match t with | .Tactic => "Tactic" @@ -44,7 +44,7 @@ structure InventoryDocEntry where userName : Name category : String content : String - deriving ToJson, Repr + deriving ToJson, Repr, Inhabited /-- Environment extension for inventory documentation. -/ initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ← @@ -118,8 +118,9 @@ structure LevelId where level : Nat deriving Inhabited -structure Availability where +structure ComputedInventoryItem where name : Name + category : String locked : Bool disabled : Bool deriving ToJson, FromJson, Repr, Inhabited @@ -132,7 +133,7 @@ structure InventoryInfo where -- only these inventory items are allowed in this level (ignored if empty): only : Array Name -- inventory items in this level (computed by `MakeGame`): - computed : Array Availability + computed : Array ComputedInventoryItem deriving ToJson, FromJson, Repr, Inhabited def getCurLevelId [MonadError m] : m LevelId := do diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index bfb4105..aab19bc 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/server/leanserver/GameServer/Game.lean @@ -42,9 +42,9 @@ Fields: structure LevelInfo where index : Nat title : String - tactics : Array Availability - lemmas : Array Availability - definitions : Array Availability + tactics : Array ComputedInventoryItem + lemmas : Array ComputedInventoryItem + definitions : Array ComputedInventoryItem introduction : String descrText : String := "" descrFormat : String := "" @@ -58,9 +58,9 @@ structure LoadLevelParams where structure DidOpenLevelParams where uri : String levelModule : Name - tactics : Array Availability - lemmas : Array Availability - definitions : Array Availability + tactics : Array ComputedInventoryItem + lemmas : Array ComputedInventoryItem + definitions : Array ComputedInventoryItem deriving ToJson, FromJson structure Doc where