chore: modify findDocString?

src/Lean/DocString.lean

@@ -17,8 +17,8 @@ def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option
   | some docString => addDocString declName docString
   | none => return ()
 
-def findDocString? [Monad m] [MonadEnv m] (declName : Name) : m (Option String) :=
-  return docStringExt.find? (← getEnv) declName
+def findDocString? (env : Environment) (declName : Name) : Option String :=
+  docStringExt.find? env declName
 
 private builtin_initialize moduleDocExt : SimplePersistentEnvExtension String (Std.PersistentArray String) ← registerSimplePersistentEnvExtension {
   name          := `moduleDocExt

src/Lean/Server/InfoUtils.lean

@@ -134,13 +134,14 @@ def Info.type? (i : Info) : MetaM (Option Expr) :=
   | _ => return none
 
 def Info.docString? (i : Info) : MetaM (Option String) := do
+  let env ← getEnv
   if let Info.ofTermInfo ti := i then
     if let some n := ti.expr.constName? then
-      return ← findDocString? n
+      return ← findDocString? env n
   if let Info.ofFieldInfo fi := i then
-    return ← findDocString? fi.projName
+    return ← findDocString? env fi.projName
   if let some ei := i.toElabInfo? then
-    return ← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind
+    return ← findDocString? env ei.elaborator <||> findDocString? env ei.stx.getKind
   return none
 
 /-- Construct a hover popup, if any, from an info node in a context.-/

tests/lean/docStr.lean

@@ -45,7 +45,7 @@ def g (x : Nat) : Nat :=
 open Lean
 
 def printDocString (declName : Name) : MetaM Unit := do
-  match (← findDocString? declName) with
+  match (← findDocString? (← getEnv) declName) with
   | some docStr => IO.println (repr docStr)
   | none => IO.println s!"doc string for '{declName}' is not available"