chore: make Verso module docstring API more like that for Markdown (#12093)

This PR makes the Verso module docstring API more like the Markdown
module docstring API, enabling downstream consumers to use them the same
way.

src/Lean/DocString/Add.lean

@@ -125,7 +125,7 @@ Parses and elaborates a Verso module docstring.
 def versoModDocString
     (range : DeclarationRange) (doc : TSyntax ``document) :
     TermElabM VersoModuleDocs.Snippet := do
-  let level := getVersoModuleDocs (← getEnv) |>.terminalNesting |>.map (· + 1)
+  let level := getMainVersoModuleDocs (← getEnv) |>.terminalNesting |>.map (· + 1)
   Doc.elabModSnippet range (doc.raw.getArgs.map (⟨·⟩)) (level.getD 0) |>.execForModule
 
 

src/Lean/DocString/Extension.lean

@@ -409,11 +409,29 @@ private builtin_initialize versoModuleDocExt :
 }
 
 
-def getVersoModuleDocs (env : Environment) : VersoModuleDocs :=
+/--
+Returns the Verso module docs for the current main module.
+
+During elaboration, this will return the modules docs that have been added thus far, rather than
+those for the entire module.
+-/
+def getMainVersoModuleDocs (env : Environment) : VersoModuleDocs :=
   versoModuleDocExt.getState env
 
+@[deprecated getMainVersoModuleDocs (since := "2026-01-21")]
+def getVersoModuleDocs := @getMainVersoModuleDocs
+
+
+/--
+Returns all snippets of the Verso module docs from the indicated module, if they exist.
+-/
+def getVersoModuleDoc? (env : Environment) (moduleName : Name) :
+    Option (Array VersoModuleDocs.Snippet) :=
+  env.getModuleIdx? moduleName |>.map fun modIdx =>
+    versoModuleDocExt.getModuleEntries (level := .server) env modIdx
+
 def addVersoModuleDocSnippet (env : Environment) (snippet : VersoModuleDocs.Snippet) : Except String Environment :=
-  let docs := getVersoModuleDocs env
+  let docs := getMainVersoModuleDocs env
   if docs.canAdd snippet then
     pure <| versoModuleDocExt.addEntry env snippet
   else throw s!"Can't add - incorrect nesting {docs.terminalNesting.map (s!"(expected at most {·})") |>.getD ""})"

src/Lean/Elab/BuiltinCommand.lean

@@ -21,7 +21,7 @@ namespace Lean.Elab.Command
 
   match stx[1] with
   | Syntax.atom _ val =>
-    if getVersoModuleDocs (← getEnv) |>.isEmpty then
+    if getMainVersoModuleDocs (← getEnv) |>.isEmpty then
       let doc := String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩)
       modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
     else