Black text on black background on hover with `linter.defProp`

[whxvd]

Tested with the current nightly-testing. In the following, the definition of p triggers the linter.defProp.

import VersoManual
open Verso Doc Genre Manual InlineLean

set_option linter.defProp true

def main := manualMain <| VersoDoc.toPart <| #doc (Manual) "MWE" =>

```lean
def p : True :=
  .intro
```

Three issues surface:

1. In VSCode the squiggly yellow line is displayed at a wrong location. (See the first image below.)

2. In the rendered document, the squiggly yellow line is drawn on the whole command. In VSCode the squiggly line appears only on the first line. (See the second image below.)

3. In the rendered document, when hovering over the code, most of it becomes black text on black background. (See the third image below.)

Here is the same using the #doc command instead of the #doc term on https://live.lean-lang.org. It surfaces the same issues.

Image 1

Image 2

Image 3