diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 5b15847a..8bd5fd50 100644 --- 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 index 47187178..4aa17fc7 100644 --- 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))