From 04038a32c8a25040d512881ea206a3ad83639367 Mon Sep 17 00:00:00 2001
From: joneugster <eugster.jon@gmail.com>
Date: Mon, 9 Oct 2023 23:25:28 +0200
Subject: [PATCH] fix inventory local storage

---
 client/src/components/infoview/main.tsx | 7 ++++++-
 client/src/state/api.ts                 | 1 +
 server/GameServer/Game.lean             | 5 +++--
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index be8017e..ce819e0 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -80,6 +80,11 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
           ...level?.definitions
         ].filter((tile) => tile.new).map((tile) => tile.name)
 
+        // Add the proven statement to the local storage as well.
+        if (level?.statementName != null) {
+          newTiles.push(level?.statementName)
+        }
+
         let inv: string[] = selectInventory(gameId)(store.getState())
 
         // add new items and remove duplicates
@@ -130,7 +135,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
 function ExerciseStatement({ data }) {
   if (!data?.descrText) { return <></> }
   return <div className="exercise-statement"><Markdown>
-    {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}`}
+    {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}`}
   </Markdown></div>
 }
 
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index 524a5a4..725c7ad 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -36,6 +36,7 @@ export interface LevelInfo {
   descrFormat: null|string,
   lemmaTab: null|string,
   statementName: null|string,
+  displayName: null|string,
   template: null|string
 }
 
diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean
index 1590d55..d668c1d 100644
--- a/server/GameServer/Game.lean
+++ b/server/GameServer/Game.lean
@@ -50,6 +50,7 @@ structure LevelInfo where
   descrText : Option String := none
   descrFormat : String := ""
   lemmaTab : Option String
+  displayName : Option String
   statementName : Option String
   template : Option String
 deriving ToJson, FromJson
@@ -165,7 +166,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
               match lvl.lemmas.tiles.find? (·.new) with
               | some tile => tile.category
               | none => none
-            statementName := match lvl.statementName with
+            statementName := lvl.statementName.toString
+            displayName := match lvl.statementName with
               | .anonymous => none
               | name => match (inventoryExt.getState env).find?
                   (fun x => x.name == name && x.type == .Lemma) with
@@ -194,7 +196,6 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
     --   return true
     | Message.request id "loadDoc" params =>
       let p ← parseParams LoadDocParams (toJson params)
-      let s ← get
       let c ← read
       let some doc ← getInventoryItem? p.name p.type
         | do