Squiggly `Lean.log` lines not shown in `lean` blocks

[whxvd]

This is not so important, but nonetheless:

import VersoManual
open Verso Doc Genre Manual InlineLean

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

```lean
run_meta Lean.logWarning "Warning"
run_meta Lean.logInfo "Info"
```

In VSCode, that does not show the usual squiggly lines under the run_metas.

[whxvd]

I started to read the source of Verso and stumbled upon the fact that this silencing of messages is explicitly implemented in order to not litter build logs. I would still like to be able to see the code blocks in the editor just the way they would appear in normal source (or in the resulting Verso output). I think it may be possible to implement the distinction by being conditional on whether elaboration occurs from lake serve or not. And controllable via options. I may look into that myself at some time.