fix: use realistic source spans for Markdown (#878)

This fixes a panic in some clients of the Markdown support that used it
to add blocks to a document after #771.

Author: david-christiansen

src/tests/Tests/VersoManual/Markdown.lean

@@ -43,6 +43,46 @@ def testAddPartFromMarkdown (input : String) : Elab.TermElabM String := do
   let (_, _, part) ← addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default
   part.partContext.priorParts.toList.map displayPartStructure |> String.join |> pure
 
+/--
+Every part produced from Markdown headers must have range and selection syntax whose recovered
+ranges satisfy the TOC invariant: the selection range lies within `[rangeStart, endPos]`. Violating
+it (position-less syntax, or an `endPos` of zero) panics in `requireValidTOCRanges` during the
+document-symbol/folding conversion.
+-/
+partial def partRangesValid : FinishedPart → Bool
+  | .mk rangeStx selectionStx _ _ _ _ subParts endPos =>
+    match rangeStx.getRange?, selectionStx.getRange? with
+    | some r, some sel => (r.start ≤ sel.start) && (sel.stop ≤ endPos) && subParts.all partRangesValid
+    | _, _ => false
+  | .included _ => true
+
+open PartElabM in
+/--
+Parses Markdown under a positioned reference and closes the document at that reference's end, as a
+real document's Markdown block elaborator would, then reports whether every resulting part has a
+valid TOC range.
+-/
+def markdownPartRangesValid (input : String) : Elab.TermElabM Bool := do
+  let some parsed := MD4Lean.parse input
+    | throwError m!"Couldn't parse markdown {input}"
+  let ref := Syntax.node (.synthetic ⟨0⟩ ⟨100⟩) identKind #[]
+  withRef ref do
+    let addParts : PartElabM Unit := do
+      let mut levels := []
+      for block in parsed.blocks do
+        levels ← addPartFromMarkdown block levels
+      closePartsUntil 0 (ref.getTailPos?.getD default)
+    let (_, _, part) ← addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default
+    return part.partContext.priorParts.all partRangesValid
+
+/-- info: true -/
+#guard_msgs in
+#eval markdownPartRangesValid r#"
+# Acknowledgements
+## Contributors
+# Another Section
+"#
+
 /--
 info:
 # header1

src/verso-manual/VersoManual/Markdown.lean

@@ -284,8 +284,11 @@ private partial def closeMarkdownSections {m} [Monad m]
   | [] => pure ()
   | docLevel :: more =>
     if docLevel ≥ level then
-      -- `default` here because the Markdown parser provides no source position
-      let some ctxt' := (← getThe PartElabM.State).partContext.close default
+      -- Markdown headers carry no source extent of their own, so end the section at the end of the
+      -- current reference. This keeps each part's range valid (the selection stays within
+      -- `[rangeStart, endPos]`) for the TOC range conversion.
+      let endPos := (← getRef).getTailPos?.getD default
+      let some ctxt' := (← getThe PartElabM.State).partContext.close endPos
         |  throwError m!"Failed to close verso part corresponding to markdown section: no parts left"
       modifyThe PartElabM.State fun st => {st with partContext := ctxt'}
       modifyThe MDState ({· with inHeaders := more})
@@ -313,7 +316,9 @@ private partial def addPartFromMarkdownAux {m} [Monad m]
       | .ok t => pure t
       | .error e => throwError m!"Unsupported Markdown in header:\n{e}"
     let titleText := titleTexts.foldl (· ++ ·) ""
-    let titleSyntax := quote (k := `str) titleText
+    -- Markdown headers have no source syntax of their own, so anchor TOC ranges to the current
+    -- reference, which has a real source position.
+    let titleSyntax ← getRef
     startMarkdownSection level {
       rangeSyntax := titleSyntax
       selectionSyntax := titleSyntax