show lemma and tactic docs

server/leanserver/GameServer/Commands.lean

@@ -250,11 +250,6 @@ elab "NewLemmas" args:ident* : command => do
 
 /-! ## Make Game -/
 
-def getTacticDoc! (tac : Name) : CommandElabM TacticDocEntry := do
-  match (tacticDocExt.getState (← getEnv)).find? (·.name = tac) with
-  | some doc => return doc
-  | none => throwError "Tactic documentation not found: {tac}"
-
 /-- Make the final Game. This command will precompute various things about the game, such as which
 tactics are available in each level etc. -/
 elab "MakeGame" : command => do

server/leanserver/GameServer/EnvExtensions.lean

@@ -41,6 +41,10 @@ initialize tacticDocExt : SimplePersistentEnvExtension TacticDocEntry (Array Tac
     addImportedFn := Array.concatMap id
   }
 
+def getTacticDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) :
+    m (Option TacticDocEntry) := do
+  return (tacticDocExt.getState (← getEnv)).find? (·.name = tac)
+
 open Elab Command in
 /-- Print a registered tactic doc for debugging purposes. -/
 elab "#print_tactic_doc" : command => do
@@ -64,6 +68,10 @@ initialize lemmaDocExt : SimplePersistentEnvExtension LemmaDocEntry (Array Lemma
     addImportedFn := Array.concatMap id
   }
 
+def getLemmaDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) :
+    m (Option LemmaDocEntry) := do
+  return (lemmaDocExt.getState (← getEnv)).find? (·.name = tac)
+
 open Elab Command in
 /-- Print a lemma doc for debugging purposes. -/
 elab "#print_lemma_doc" : command => do

server/leanserver/GameServer/Game.lean

@@ -53,6 +53,32 @@ structure LoadLevelParams where
   level : Nat
   deriving ToJson, FromJson
 
+structure Doc where
+  name: String
+  text: String
+deriving ToJson
+
+inductive TacOrLem := | tactic | «lemma»
+deriving ToJson, FromJson
+
+structure LoadDocParams where
+  name : Name
+  type : TacOrLem
+deriving ToJson, FromJson
+
+def mkDoc (name : Name) (type : TacOrLem) : GameServerM (Option Doc) := do
+  match type with
+  | .tactic => do
+    let doc ← getTacticDoc? name
+    return doc.map fun doc =>
+      { name := doc.name.toString
+        text := doc.content }
+  | .lemma => do
+    let doc ← getLemmaDoc? name
+    return doc.map fun doc =>
+      { name := doc.name.toString
+        text := doc.content }
+
 partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
   match ev with
   | ServerEvent.clientMsg msg =>
@@ -68,8 +94,9 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let c ← read
       let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level}
         | do
-            c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩
-            return true
+          c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩
+          return true
+
       let levelInfo : LevelInfo :=
           { index := lvl.index,
             title := lvl.title,
@@ -80,6 +107,16 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
             introduction := lvl.introduction }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
       return true
+    | Message.request id "loadDoc" params =>
+      let p ← parseParams LoadDocParams (toJson params)
+      let s ← get
+      let c ← read
+      let some doc ← mkDoc p.name p.type
+        | do
+            c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Documentation not found: {p.name}", none⟩
+            return true
+      c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
+      return true
     | _ => return false
   | _ => return false