Add tabs for lemmas #23

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)

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

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