At least in the Manual genre with HTML output, it happens that there are two hover messages at a single code element. Example:
import VersoManual
open Verso Doc Genre Manual InlineLean
set_option linter.unusedVariables true
def main := manualMain <| VersoDoc.toPart <| #doc (Manual) "MWE" =>
+ Introduce some vertical space so that popups always appear above
+ Vertical space
+ Vertical space
+ Vertical space
+ Vertical space
+ Vertical space
```lean
def u := fun x : Nat => ()
#eval 23
#eval 42
```
Hovering over the x shows two popups (the type of x and the linter.unusedVariables message). Hovering over #eval shows the docstring of #eval, which occludes the resulting value. Tested with the current nightly-testing. Here is a version on https://live.lean-lang.org.
In VSCode multiple messages at a single location get aggregated into a single popup. I personally do not like popups on hover, especially such large ones, at all. Ideally there would also be an option to switch off automatic popups, and show (and possibly cycle) them on explicit clicking only.
Topic on Zulip.
At least in the
Manualgenre with HTML output, it happens that there are two hover messages at a single code element. Example:Hovering over the
xshows two popups (the type ofxand thelinter.unusedVariablesmessage). Hovering over#evalshows the docstring of#eval, which occludes the resulting value. Tested with the currentnightly-testing. Here is a version on https://live.lean-lang.org.In VSCode multiple messages at a single location get aggregated into a single popup. I personally do not like popups on hover, especially such large ones, at all. Ideally there would also be an option to switch off automatic popups, and show (and possibly cycle) them on explicit clicking only.
Topic on Zulip.