section appears as namespace in breadcrumb

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

In VSCode, the breadcrumb tooltip calls sections namespaces.

Steps to Reproduce

In an empty file, put

section Foo

end Foo

and put the cursor on the second line and the mouse over the Foo word in the top breadcrumb in VSCode.

Expected behavior: [What you expect to happen]

Get a tooltip saying Foo (section).

Actual behavior: [What actually happens]

Get a tooltip saying Foo (namespace).

Reproduces how often: [What percentage of the time does it reproduce?]

Always

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Lean (version 4.0.0-nightly-2022-12-23, commit 0553b5936e46, Release) on Linux. VSCode 1.73.1 with extension v0.0.99.

Reproduce the issue in VSCode with the supplied section Foo snippet and inspect the breadcrumb tooltip in extension v0.0.99. Confirm that the tooltip identifies Foo as a section rather than a namespace; the issue does not name an implementation file or test to run.