fix inventory local storage

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>
 }
 

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
 }
 

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