`handleDocumentSymbol` returns an incomplete list of declarations

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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 current handleDocumentSymbol implementation only considers top-level syntax before any elaboration or macro expansion. As a result, declarations like Mathlib's lemmas or even declarations inside open ... in blocks are not reported by the server (in response to textDocument/documentSymbol).

Context

I first discussed it in Zulip. I noticed the server did not include lemma declarations in the document symbols (which I use frequently to navigate in files through Emacs' consult-imenu).

Steps to Reproduce

1. Write, in a file,

   open Lean in
   theorem foo : 1 = 1 := rfl
   
   macro "stupid" dec:command : command => pure dec
   
   stupid def bar := 1
   

2. In some editor with LSP support, check document symbols. For instance, in VSCode, this can be seen by clicking the three dots in the header line.

Expected behavior: foo and bar are reported as document symbols
Actual behavior: foo and bar are missing from document symbols

Versions

4.24.0-nightly-2025-08-30

Additional Information

I wrote a fix (my purpose when writing it was to learn more about Lean internals):

https://github.com/estradilua/lean4/commit/9c48fd4c3ad6de81b2dd590c4f8893e743be8b16

If you think it's acceptable, I can create a PR.

Impact

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

Start at the Lean language server's handleDocumentSymbol implementation and reproduce the issue with the open ... in, macro, theorem, and definition example from the report. Compare the returned document symbols with the expected foo and bar declarations; done means declarations introduced through elaboration or macro expansion are reported.