From 67090f53faeea423ce60c6ddc43c24beef882bad Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 18 Jun 2024 15:40:35 +0200
Subject: [PATCH] add basic infos to inventory

---
 client/src/components/inventory.tsx  | 10 ++++++++++
 server/GameServer/EnvExtensions.lean |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
index 09074097..67c31283 100644
--- a/client/src/components/inventory.tsx
+++ b/client/src/components/inventory.tsx
@@ -229,6 +229,16 @@ export function Documentation() {
     <h1 className="doc">{docTile.displayName}</h1>
     <p><code>{docEntry.data?.statement}</code></p>
     <Markdown>{t(docEntry.data?.content, {ns: gameId})}</Markdown>
+    {/* TODO: The condition below should be updated so that the section
+    is displayed whenever it's non-empty. */}
+    {docTile.proven && <>
+        <h2>Further details</h2>
+        <ul>
+          {docTile.proven && <li>Proven in: <a href={`#/${gameId}/world/${docTile.world}/level/${docTile.level}`}>{docTile.world} level {docTile.level}</a></li>}
+        </ul>
+      </>
+    }
+
   </div>
 }
 
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index cbe3f045..831bb914 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -109,7 +109,7 @@ structure InventoryTile where
   hidden := false
   /-- hover text -/
   altTitle : String := default
-deriving ToJson, FromJson, Repr, Inhabited
+deriving ToJson, FromJson, Repr, Inhabited, BEq
 
 def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
       name := item.name,