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.

[david-christiansen]

I totally get that this would be nice. This is a tricky area, however, with lots of weird corner cases.

If we log errors, then the file is treated as "failed to elaborate", which is definitely not what we want for expected errors. And I'm hesitant to make the behavior differ too much based on whether it's in the language server - that can lead to bugs that are difficult to address.

We also don't have a good way to distinguish between "error shown in user code that we expect" and "unexpected error from user code that's honestly an error".

I think that really figuring all this out may involve Lean changes. It's worth doing.