Parser docstring vs syntax hover target audience confusion

Description

A lot of parser and parser combinators have docstrings that aim to explain how to use the the parser, but then they end up being shown to the unsuspecting user when hovering over a piece of syntax that doesn't happen to have a better docstring.

For example in

import Lean
/-- docstring -/
theorem foo : True := trivial

if you hover over the : you get

declSig matches the signature of a declaration with required type: a list of binders and then : type 

and if you hover over the docstring you get

A docComment parses a…

Depending whether you already have #3918 you need import Lean to make these hovers visible, but note that import Mathlib implies import Lean, so that’s not the core issue.

It seems that one needs at least a way to indicate “the docstring of this parser or syntax is not meant for hovers”, and going through the code to annotate all docstrings that don’t have a useful user-facing docstring.

A more thorough solution is to somehow be able to write two docstrings, one to document Lean.Parser.Command.declSig, and one to show upon hovering : above.

Versions

Around 4.12.0

Impact

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

Start by reproducing the declSig and docComment hover behavior from the import Lean example, focusing on parser docstrings and the : syntax hover. Review the documentation and hover behavior around Lean.Parser.Command.declSig; done means parser-oriented text is not shown as unrelated syntax help, or separate parser and hover documentation can be provided.