From 2c48ae7dfbc40059ec04cd0a702b34a144091d40 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Thu, 22 Jan 2026 05:45:49 +0100
Subject: [PATCH] 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       |  2 +-
 src/Lean/DocString/Extension.lean | 22 ++++++++++++++++++++--
 src/Lean/Elab/BuiltinCommand.lean |  2 +-
 3 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean
index 8e90af5338..d34ff23b38 100644
--- a/src/Lean/DocString/Add.lean
+++ b/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
 
 
diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean
index f199087f40..5961765dcc 100644
--- a/src/Lean/DocString/Extension.lean
+++ b/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 ""})"
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 19bb8f2f64..9fdddb0231 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/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