fix: hide hidden inventory items in overview #169

leanprover-community · Dec 14, 2023 · ae636a0 · ae636a0
1 parent 5aa0764
commit ae636a0
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 14 deletions.
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
@@ -819,7 +819,7 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
-            hidden := levelInfo.hidden.contains item }
+            hidden := hiddenItems.contains item }
 
         -- add the exercise statement from the previous level
         -- if it was named
@@ -851,4 +851,16 @@ elab "MakeGame" : command => do
           return level.setComputedInventory inventoryType itemsArray
     allItemsByType := allItemsByType.insert inventoryType allItems
 
-  saveGameData allItemsByType
+  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
+    (allItemsByType.findD type {}).toArray.mapM (fun name => do
+      let some item ← getInventoryItem? name type
+        | throwError "Expected item to exist: {name}"
+      return item.toTile)
+  let inventory : InventoryOverview := {
+    lemmas := (← getTiles .Lemma).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    definitions := (← getTiles .Definition).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    lemmaTab := none
+  }
+
+  saveGameData allItemsByType inventory
diff --git a/server/GameServer/SaveData.lean b/server/GameServer/SaveData.lean
@@ -27,7 +27,8 @@ def copyImages : IO Unit := do
 #eval IO.FS.createDirAll ".lake/gamedata/"
 
 -- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
+    (inventory : InventoryOverview): CommandElabM Unit := do
   let game ← getCurGame
   let env ← getEnv
   let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
@@ -51,15 +52,4 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : Comma
         | throwError "Expected item to exist: {name}"
       IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
 
-  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
-    (allItemsByType.findD type {}).toArray.mapM (fun name => do
-      let some item ← getInventoryItem? name type
-        | throwError "Expected item to exist: {name}"
-      return item.toTile)
-  let inventory : InventoryOverview := {
-    lemmas := ← getTiles .Lemma
-    tactics := ← getTiles .Tactic
-    definitions := ← getTiles .Definition
-    lemmaTab := none
-  }
   IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))