Verso docstrings and `#guard_msgs` cause panic: unexpected context-free info tree node

[Vierkantor]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The combination of #guard_msgs and Verso docstrings that send messages seems to cause panics under certain conditions: "PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:66:21: unexpected context-free info tree node".

Example:

set_option doc.verso true

-- Panic message on the line below:
/--
error: Unexpected warning:
  declaration uses `sorry`

Hint: The `+error` flag indicates that warnings are expected:
  lean ̲+̲w̲a̲r̲n̲i̲n̲g̲
-/
#guard_msgs in
/-!
```lean
theorem int_eq_nat {z : Int} : ∃ n, Int.ofNat n = z := sorry
```
-/

A #guard_msgs inside of a Verso docstring behaves similarly:

set_option doc.verso true

/-!
```lean
@[simp]
theorem what : False := sorry

/-- error: simp made no progress -/
#guard_msgs in
attribute [-simp] what in
example : False := by simp
```
-/

Context

Noticed this before when debugging Mathlib's header style linter and found a good reproducible example when minimizing for #12064.

Steps to Reproduce

1. Write a Verso docstring that outputs messages, such as a warning or error.
2. Write #guard_msgs in before the Verso docstring, or in a code block inside the Verso docstring.

Expected behavior: No panics.

Actual behavior: Panic due to context-free info tree node.

Versions

Lean 4.27.0-rc1 (Mathlib, MacOS / Darwin Kernel Version 23.6.0 / arm64), Lean 4.28.0-nightly-2026-01-19 (Lean4web nightly)

Additional Information

n/a

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.