From 780514e45abb6b57af9904ba118959e3e61c9f46 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 14 Feb 2024 18:22:01 +0100 Subject: [PATCH] fix: allow theorems from inventory #191 --- server/GameServer/FileWorker.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index b720002..2d4f6b1 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -169,15 +169,20 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : match theoremsAndDefs.find? (·.name == n) with | none => -- Theorem will never be introduced in this game - addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" + addMessageByDifficulty info s!"The theorem/definition '{n}' is not available in this game!" | some thm => -- Theorem is introduced at some point in the game. if thm.disabled then -- Theorem is disabled in this level. addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!" else if thm.locked then - -- Theorem is still locked. - addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" + match workerState.inventory.find? (· == n.toString) with + | none => + -- Theorem is still locked. + addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" + | some _ => + -- Theorem is in the inventory, allow it. + pure () where addMessageByDifficulty (info : SourceInfo) (s : MessageData) := -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors