add display names for definitions and lemmas

server/leanserver/GameServer/Commands.lean

@@ -303,14 +303,21 @@ def checkInventoryDoc (type : InventoryType) (name : Name) : CommandElabM Unit :
 
 /-! ### Tactics -/
 
-/-- Declare a documentation entry for some tactic.
-Expect an identifier and then a string literal. -/
+/-- Documentation entry of a tactic. Example:
+
+```
+TacticDoc rw "`rw` stands for rewrite, etc. "
+```
+
+* The identifier is the tactics name. Some need to be escaped like `«have»`.
+* The description is a string supporting Markdown.
+ -/
 elab "TacticDoc" name:ident content:str : command =>
   modifyEnv (inventoryDocExt.addEntry · {
     category := default
     type := .Tactic
     name := name.getId,
-    userName := name.getId,
+    displayName := name.getId.toString,
     content := content.getString })
 
 /-- Declare tactics that are introduced by this level. -/
@@ -333,14 +340,23 @@ elab "OnlyTactic" args:ident* : command => do
 
 /-! ### Definitions -/
 
-/-- Declare a documentation entry for some definition.
-Expect an identifier and then a string literal. -/
-elab "DefinitionDoc" name:ident content:str : command =>
+/-- Documentation entry of a definition. Example:
+
+```
+DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Surjective`, etc."
+```
+
+* The first identifier is used in the commands `[New/Only/Disabled]Definition`.
+  It is preferably the true name of the definition. However, this is not required.
+* The string following `as` is the displayed name (in the Inventory).
+* The description is a string supporting Markdown.
+ -/
+elab "DefinitionDoc" name:ident "as" displayName:str content:str : command =>
   modifyEnv (inventoryDocExt.addEntry · {
     category := default
     type := .Definition
     name := name.getId,
-    userName := name.getId,
+    displayName := displayName.getString,
     content := content.getString })
 
 /-- Declare definitions that are introduced by this level. -/
@@ -364,15 +380,23 @@ elab "OnlyDefinition" args:ident* : command => do
 
 /-! ### Lemmas -/
 
-/-- Declare a documentation entry for some lemma.
-Expect two identifiers and then a string literal. The first identifier is meant
-as the real name of the lemma while the second is the displayed name. Currently
-the real name isn't used. -/
-elab "LemmaDoc" name:ident "as" userName:ident "in" category:str content:str : command =>
+/-- Documentation entry of a lemma. Example:
+
+```
+LemmaDoc Nat.succ_pos as "succ_pos" in Nat "says `0 < n.succ`, etc."
+```
+
+* The first identifier is used in the commands `[New/Only/Disabled]Lemma`.
+  It is preferably the true name of the lemma. However, this is not required.
+* The string following `as` is the displayed name (in the Inventory).
+* The identifier after `in` is the category to group lemmas by (in the Inventory).
+* The description is a string supporting Markdown.
+ -/
+elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
   modifyEnv (inventoryDocExt.addEntry · {
     name := name.getId,
     type := .Lemma
-    userName := userName.getId,
+    displayName := displayName.getString,
     category := category.getString,
     content := content.getString })
 
@@ -430,9 +454,11 @@ elab "MakeGame" : command => do
     let Availability₀ : HashMap Name ComputedInventoryItem :=
       HashMap.ofList $
         ← allItems.toList.mapM fun name => do
+          let data := (← getInventoryDoc? name inventoryType).get!
           return (name, {
             name
-            category := (← getInventoryDoc? name inventoryType).get!.category
+            displayName := data.displayName
+            category := data.category
             locked := true
             disabled := false})
 
@@ -443,9 +469,11 @@ elab "MakeGame" : command => do
       let predecessors := game.worlds.predecessors worldId
       for predWorldId in predecessors do
         for item in newItemsInWorld.find! predWorldId do
+          let data := (← getInventoryDoc? item inventoryType).get!
           items := items.insert item {
             name := item
-            category := (← getInventoryDoc? item inventoryType).get!.category
+            displayName := data.displayName
+            category := data.category
             locked := false
             disabled := false
           }
@@ -458,13 +486,25 @@ elab "MakeGame" : command => do
 
       for (levelId, level) in levels do
         for item in (level.getInventory inventoryType).new do
-          let category := (← getInventoryDoc? item inventoryType).get!.category
-          items := items.insert item {name := item, category, locked := false, disabled := false}
+          let data := (← getInventoryDoc? item inventoryType).get!
+          items := items.insert item {
+            name := item
+            displayName := data.displayName
+            category := data.category
+            locked := false
+            disabled := false
+          }
 
         let mut disabled : HashSet Name := {}
         for item in (level.getInventory inventoryType).disabled do
-          let category := (← getInventoryDoc? item inventoryType).get!.category
-          items := items.insert item {name := item, category, locked := false, disabled := false}
+          let data := (← getInventoryDoc? item inventoryType).get!
+          items := items.insert item {
+            name := item
+            displayName := data.displayName
+            category := data.category
+            locked := false
+            disabled := false
+          }
           -- (we set disabled to false at first because it applies only to the current level)
           disabled := disabled.insert item
 

server/leanserver/GameServer/EnvExtensions.lean

@@ -43,7 +43,7 @@ instance : ToString InventoryType := ⟨fun t => match t with
 structure InventoryDocEntry where
   name : Name
   type : InventoryType
-  userName : Name
+  displayName : String
   category : String
   content : String
   deriving ToJson, Repr, Inhabited
@@ -122,6 +122,7 @@ deriving Inhabited
 
 structure ComputedInventoryItem where
   name : Name
+  displayName : String
   category : String
   locked : Bool
   disabled : Bool

server/leanserver/GameServer/Game.lean

@@ -66,6 +66,7 @@ structure DidOpenLevelParams where
 
 structure Doc where
   name: String
+  displayName: String
   text: String
 deriving ToJson
 
@@ -80,7 +81,7 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
   -- Execute the regular handling of the `didOpen` event
   handleDidOpen p
   let fw ← findFileWorker! m.uri
-  let s ← get
+  -- let s ← get
   let c ← read
   let some lvl ← GameServer.getLevelByFileName? ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString)
     | do
@@ -132,7 +133,7 @@ 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 s ← get
       let c ← read
       let some doc ← getInventoryDoc? p.name p.type
         | do
@@ -140,6 +141,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
             return true
       let doc : Doc :=
           { name := doc.name.toString
+            displayName := doc.displayName
             text := doc.content }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
       return true