fix: label external declaration sections without h1 (#880)

This PR renders Manual docstring subsection labels as accessible labeled
groups instead of nested `h1` elements inside external declaration
bodies.

The previous HTML used `h1` tags for labels such as `Fields` and
`Constructors`, which made them part of the document heading outline
even though they only name declaration detail groups. This can confuse
heading navigation for screen readers.

The new `Html.labeledGroup` helper renders a visible paragraph label,
connects it to a `role="group"` container with `aria-labelledby`, and
lets downstream renderers reuse the same accessibility pattern without
hand-rolling it. Blueprint has already validated this shape downstream
with Firefox accessibility tooling.

Thanks to @NicolasRouquette for the original bug report:
leanprover/verso-blueprint#130

Author: ejgallego

src/tests/Tests/VersoManual/Html.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 import VersoManual.Html
+import VersoManual
 
 namespace Verso.Genre.Manual.Html
 
@@ -112,3 +113,76 @@ Done
       break
 
 end
+
+namespace DocstringSectionRegression
+
+open Verso
+open Verso.Output
+open Verso.Genre.Manual
+
+/-- A fixture for Manual docstring subsection HTML rendering. -/
+structure SectionFixture where
+  /-- Field documentation. -/
+  field : Nat
+
+/-- A fixture for Manual docstring constructor subsection HTML rendering. -/
+inductive ConstructorFixture where
+  /-- Constructor documentation. -/
+  | intro : ConstructorFixture
+
+#docs (Manual) doc "Docstring section labels" :=
+:::::::
+
+{docstring SectionFixture}
+
+{docstring ConstructorFixture}
+
+:::::::
+
+private def hasSubstring (s sub : String) : Bool :=
+  s.find? sub |>.isSome
+
+private def compactHtml (s : String) : String :=
+  s.foldl (init := "") fun out c =>
+    if c.isWhitespace then out else out.push c
+
+private def renderDoc : IO String := do
+  let rendered ← IO.mkRef ""
+  let exitCode ← withLogger fun logger => do
+    let cfg : RenderConfig := {}
+    let (part, state) ← (traverseHtmlSingle cfg doc.toPart).run extension_impls% |>.run logger
+    let ctxt : Manual.TraverseContext := {}
+    let definitionIds := state.definitionIds ctxt
+    let remotes : Multi.AllRemotes := {}
+    let linkTargets := cfg.linkTargets state remotes
+    let (html, _) ←
+      (Manual.toHtml (m := ReaderT Multi.AllRemotes (ReaderT ExtensionImpls (BuildLogT IO)))
+          {} ctxt state definitionIds linkTargets {} part).run {}
+        |>.run remotes
+        |>.run extension_impls%
+        |>.run logger
+    rendered.set html.asString
+  unless exitCode == 0 do
+    throw <| IO.userError "Manual docstring HTML rendering logged errors"
+  rendered.get
+
+private def assertLabeledSection (compact label : String) : IO Unit := do
+  let id := s!"docstring-section-{label}"
+  let group := s!"<divclass=\"docstring-section\"role=\"group\"aria-labelledby=\"{id}\">"
+  unless hasSubstring compact group do
+    throw <| IO.userError s!"{label} section should render as a named group"
+  let labelHtml := s!"<pclass=\"docstring-section-label\"id=\"{id}\">{label}</p>"
+  unless hasSubstring compact labelHtml do
+    throw <| IO.userError s!"{label} section should use a paragraph label with the group's ID"
+  if hasSubstring compact s!"<h1>{label}</h1>" then
+    throw <| IO.userError s!"{label} section label should not render as h1"
+
+/--
+info: docstring section labels render as labeled groups
+-/
+#guard_msgs in
+#eval show IO Unit from do
+  let compact := compactHtml (← renderDoc)
+  assertLabeledSection compact "Fields"
+  assertLabeledSection compact "Constructors"
+  IO.println "docstring section labels render as labeled groups"

src/verso-manual/VersoManual/Docstring.lean

@@ -392,13 +392,18 @@ def docstringStyle := r#"
   color: #555;
 }
 
-.namedocs h1 {
-  font-size: inherit;
-  font-weight: bold
+.namedocs .docstring-section {
   margin-top: 1rem;
   margin-bottom: 1rem;
 }
 
+.namedocs .docstring-section-label {
+  font-size: inherit;
+  font-weight: bold;
+  margin-top: 0;
+  margin-bottom: 1rem;
+}
+
 .namedocs > .text .constructor {
   padding-top: 0;
   padding-right: 0;
@@ -521,21 +526,35 @@ where
 
 @[block_extension Block.docstringSection]
 def docstringSection.descr : BlockDescr where
-  traverse _ _ _ := pure none
+  traverse id info _ := do
+    let .ok header := FromJson.fromJson? (α := String) info
+      | reportError "Failed to deserialize docstring section data while traversing"; return none
+    let path ← (·.path) <$> read
+    let _ ← externalTag id path s!"docstring-section-{header}"
+    pure none
   toTeX := some fun _goI goB _id info contents =>
     open Verso.Output.TeX in do
     let .ok header := FromJson.fromJson? (α := String) info
       | reportError "Failed to deserialize docstring section data while generating TeX"; return .empty
     pure \TeX{\par\noindent\textbf{\Lean{header}}\par " " \Lean{.seq (← contents.mapM goB)}}
-  toHtml := some fun _goI goB _id info contents =>
+  toHtml := some fun _goI goB id info contents =>
     open Verso.Doc.Html HtmlT in
     open Verso.Output Html in do
       let .ok header := FromJson.fromJson? (α := String) info
-        | do reportError "Failed to deserialize docstring section data while generating HTML"; pure .empty
-      return {{
-        <h1>{{header}}</h1>
-        {{← contents.mapM goB}}
-      }}
+        | do reportError "Failed to deserialize docstring section data while generating HTML"; pure Html.empty
+      let xref : TraverseState ← HtmlT.state (genre := Manual)
+      match xref.externalTags[id]? with
+      | none =>
+        reportError s!"No HTML ID registered for docstring section '{header}'"
+        pure Html.empty
+      | some dest =>
+        let renderedContents ← contents.mapM goB
+        pure (Html.labeledGroup
+          "docstring-section"
+          "docstring-section-label"
+          (toString dest.htmlId)
+          header
+          (.seq renderedContents))
 
 @[block_extension Block.internalSignature]
 def internalSignature.descr : BlockDescr where

src/verso/Verso/Output/Html.lean

@@ -186,6 +186,28 @@ namespace Html
 /-- The default `DOCTYPE` for HTML5. -/
 public abbrev doctype := "<!DOCTYPE html>"
 
+/--
+Wrap content in a named group whose visible label should not participate in the document heading
+outline.
+
+Use this for labels that name a grouped region for assistive technology, but are not section
+headings. The label is rendered as a paragraph and connected to the group with `aria-labelledby`.
+-/
+public def labeledGroup
+    (groupClass labelClass id label : String)
+    (contents : Html) : Html :=
+  let groupAttrs :=
+    (if groupClass.isEmpty then #[] else #[("class", groupClass)]) ++
+      #[("role", "group"), ("aria-labelledby", id)]
+  let labelAttrs :=
+    (if labelClass.isEmpty then #[] else #[("class", labelClass)]) ++
+      #[("id", id)]
+  .tag "div" groupAttrs <|
+    .seq #[
+      .tag "p" labelAttrs (.text true label),
+      contents
+    ]
+
 /--
 Visit the entire tree, applying rewrites in some monad. Return `none` to signal that no rewrites are
 to be performed.