diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean index 2e7555f81f..859df742bc 100644 --- a/src/Lean/DocString.lean +++ b/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 diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index a50f534f32..8a809a2c2e 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/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.-/ diff --git a/tests/lean/docStr.lean b/tests/lean/docStr.lean index c452c2fbac..0b51642312 100644 --- a/tests/lean/docStr.lean +++ b/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"