Fix guard msgs docstring

src/tests/VersoTests/LiterateHtml.lean

@@ -302,6 +302,22 @@ private def testUnknownExtensionFallback : Test := do
   assertContains "THIS IS THE FALLBACK" html
     "HTML missing 'THIS IS THE FALLBACK' marker. The conversion's fallback children were not rendered."
 
+/--
+The doc comment on a `#guard_msgs` command is not documentation. Instead, it is a specification of
+the expected messages from the wrapped command. It must not be attributed to the declaration in that
+command as a second docstring.
+-/
+private def testGuardMsgsDocstring (data : TestData) : IO Unit := withTestDir data fun jsonDir htmlDir _ _ => do
+  runLiterateHtml jsonDir htmlDir
+  let html ← IO.FS.readFile (htmlDir / "LitConfig" / "GuardMsgs" / "index.html")
+  let docstring := "A theorem whose proof is left open."
+  let occurrences := (html.splitOn docstring).length - 1
+  unless occurrences == 1 do
+    throw <| IO.userError s!"Expected the docstring of `guarded` once in the HTML, found it {occurrences} times. \
+      The expected-messages comment of `#guard_msgs` was attributed to `guarded` as a docstring."
+  unless hasSubstring html "declaration uses" do
+    throw <| IO.userError "The expected-messages comment of `#guard_msgs` is missing from the HTML."
+
 /-- Excluded modules produce no HTML output and are absent from the navbar. -/
 private def testExclude (data : TestData) : Test := withTestDir data fun jsonDir htmlDir planFile tomlFile => do
   IO.FS.writeFile tomlFile "exclude = [\"LitConfig.NoDocstrings\"]\n"
@@ -1205,14 +1221,15 @@ private def htmlTests (data : TestData) (projectDir : System.FilePath) : List (S
   ("all built-in doc roles", testAllBuiltinDocRoles data),
   ("custom literate handlers", testCustomLiterateHandlers data),
   ("docstring code block messages", testDocstringCodeBlockMessages data),
+  ("guard_msgs docstring", testGuardMsgsDocstring data),
   ("unknown extension fallback", testUnknownExtensionFallback)
 ]
 
 /-- The literate HTML generator produces the expected output for the single-root test project. -/
 @[test]
 def literateHtml : Test := do
   let projectDir := "test-projects/literate-config"
-  let modules := #["LitConfig", "LitConfig.Core", "LitConfig.Core.Basic", "LitConfig.NoDocstrings", "LitConfig.Builtins", "LitConfig.UserExt"]
+  let modules := #["LitConfig", "LitConfig.Core", "LitConfig.Core.Basic", "LitConfig.NoDocstrings", "LitConfig.Builtins", "LitConfig.UserExt", "LitConfig.GuardMsgs"]
 
   -- First verify test project toolchain matches root toolchain
   let rootToolchain := (← IO.FS.readFile "lean-toolchain").trimAscii

src/verso-literate/VersoLiterateMain.lean

@@ -144,7 +144,12 @@ def findHighestM [Monad m] (stx : Syntax) (fn : Syntax → Option α) : m (Array
 Finds the definition sites of each constant in an info tree, and replaces each docstring with a
 reference to the definition for later substitution.
 -/
-def findDocstringDefs (stx : Syntax) (t : InfoTree) : TermElabM Syntax := do
+partial def findDocstringDefs (stx : Syntax) (t : InfoTree) : TermElabM Syntax := do
+  -- `#guard_msgs` takes the messages it expects as a doc comment, but it's not really
+  -- documentation. It must not be attached to the declaration in the command that `#guard_msgs`
+  -- wraps.
+  if stx.isOfKind ``Lean.guardMsgsCmd then
+    return stx.setArg 4 (← findDocstringDefs stx[4] t)
   -- Find the definition sites of all constants in this info tree
   let defSites := t.deepestNodes fun _ i _ =>
     match i with

test-projects/literate-config/LitConfig.lean

@@ -3,6 +3,7 @@ import LitConfig.NoDocstrings
 import LitConfig.Builtins
 import LitConfig.UserExt
 import LitConfig.Gallery
+import LitConfig.GuardMsgs
 import Verso
 
 /-!

test-projects/literate-config/LitConfig/GuardMsgs.lean

@@ -0,0 +1,11 @@
+/-!
+# Guarded Messages
+
+{lit}`#guard_msgs` takes the messages that it expects as a doc comment. That comment is not really
+documentation, so the declaration in the guarded command keeps its own docstring, and only that.
+-/
+
+/-- warning: declaration uses `sorry` -/
+#guard_msgs in
+/-- A theorem whose proof is left open. -/
+theorem guarded : 1 + 1 = 2 := sorry