In some VSCode extensions one can press control to get extra info in the popup already shown when one hovers a symbol.
In MathComp we have a command HB.about (akin to About) which prints extra info very relevant to the context of this library.
We would like to have this info printed somehow.
Some naive questions:
is the "show more" an additional query to the language server?
would it make sense to piggy back on About making it extensible on the Coq side (eg in MathComp when you call About you also call HB.about)?
gares
commented
1 year ago
In some VSCode extensions one can press control to get extra info in the popup already shown when one hovers a symbol. In MathComp we have a command
HB.about(akin toAbout) which prints extra info very relevant to the context of this library.We would like to have this info printed somehow.
Some naive questions:
Aboutmaking it extensible on the Coq side (eg in MathComp when you callAboutyou also callHB.about)?