From 25f2f0830935aa18bcb5ae3ca7c0c4e4f9613bc9 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 12 Aug 2023 12:50:26 +0200 Subject: [PATCH] fix inventory overview --- server/GameServer/Game.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean index 18207b5..58b9ec4 100644 --- a/server/GameServer/Game.lean +++ b/server/GameServer/Game.lean @@ -189,12 +189,12 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do let some game ← getGame? s.game | return false -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world - -- and reset `new`, `disabled` and `unlocked` - match game.worlds.nodes.toList with - | [] => return false - | ⟨worldId, _⟩ :: _ => + -- and reset `new`, `disabled` and `unlocked`. + -- Note: as we allow worlds without any levels (for developing), we might need + -- to try until we find the first world with levels. + for ⟨worldId, _⟩ in game.worlds.nodes.toList do let some lvl ← getLevel? {game := s.game, world := worldId, level := 1} - | do return false + | do continue let inventory : InventoryOverview := { tactics := lvl.tactics.tiles.map ({ · with locked := true, disabled := false, new := false }), @@ -207,6 +207,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do let c ← read c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩ return true + return false | _ => return false | _ => return false